### Nuprl Lemma : sqntype_product

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

Proof

Definitions occuring in Statement :  sqntype: `sqntype(n;T)` nat: `ℕ` uimplies: `b 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: `b supposing a` sqntype: `sqntype(n;T)` all: `∀x:A. B[x]` implies: `P `` 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

Latex:
\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