Nuprl Lemma : l_treeco_wf

[L,T:Type].  (l_treeco(L;T) ∈ Type)


Proof




Definitions occuring in Statement :  l_treeco: l_treeco(L;T) uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T l_treeco: l_treeco(L;T) so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  corec_wf ifthenelse_wf eq_atom_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin lambdaEquality productEquality atomEquality instantiate hypothesisEquality tokenEquality hypothesis universeEquality voidEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[L,T:Type].    (l\_treeco(L;T)  \mmember{}  Type)



Date html generated: 2018_05_22-PM-09_38_15
Last ObjectModification: 2015_12_28-PM-06_41_44

Theory : labeled!trees


Home Index