Nuprl Lemma : sqn+1type_product
∀[T,S:Type]. ∀[n:ℕ]. (sqntype(n + 1;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],
add: n + m,
natural_number: $n,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T,
so_lambda: λ2x.t[x],
so_apply: x[s],
all: ∀x:A. B[x],
prop: ℙ
Lemmas referenced :
sqn+1type_dep_product,
sqntype_wf,
nat_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
lambdaEquality,
independent_isectElimination,
hypothesis,
lambdaFormation,
because_Cache,
universeEquality
Latex:
\mforall{}[T,S:Type]. \mforall{}[n:\mBbbN{}]. (sqntype(n + 1;T \mtimes{} S)) supposing (sqntype(n;S) and sqntype(n;T))
Date html generated:
2019_06_20-AM-11_34_02
Last ObjectModification:
2018_08_17-PM-04_44_53
Theory : int_1
Home
Index