Nuprl Lemma : co-cons_wf

[T:Type]. ∀[x:T]. ∀[L:colist(T)].  ([x L] ∈ colist(T))


Proof




Definitions occuring in Statement :  co-cons: [x L] colist: colist(T) uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T co-cons: [x L] subtype_rel: A ⊆B
Lemmas referenced :  colist_wf istype-universe product_subtype_colist
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule independent_pairEquality hypothesisEquality applyEquality hypothesis sqequalHypSubstitution axiomEquality equalityTransitivity equalitySymmetry Error :universeIsType,  extract_by_obid isectElimination thin Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  Error :inhabitedIsType,  instantiate universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[L:colist(T)].    ([x  /  L]  \mmember{}  colist(T))



Date html generated: 2019_06_20-PM-00_38_12
Last ObjectModification: 2018_12_04-PM-00_20_06

Theory : list_0


Home Index