Nuprl Lemma : sqntype_product

[T,S:Type]. ∀[n:ℕ].  (sqntype(n;T × S)) supposing (sqntype(n;S) and sqntype(n;T))


Definitions occuring in Statement :  sqntype: sqntype(n;T) nat: uimplies: supposing a uall: [x:A]. B[x] product: x:A × B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a sqntype: sqntype(n;T) all: x:A. B[x] implies:  Q prop: nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A
Lemmas referenced :  sqn+1type_product equal-wf-base base_wf sqntype_wf nat_wf sqequal_n_add false_wf le_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination lambdaFormation dependent_functionElimination independent_functionElimination productEquality universeEquality Error :axiomSqequalN,  dependent_set_memberEquality natural_numberEquality sqequalRule independent_pairFormation

\mforall{}[T,S:Type].  \mforall{}[n:\mBbbN{}].    (sqntype(n;T  \mtimes{}  S))  supposing  (sqntype(n;S)  and  sqntype(n;T))

Date html generated: 2019_06_20-AM-11_34_04
Last ObjectModification: 2018_08_17-PM-03_51_00

Theory : int_1

Home Index