Nuprl Lemma : co-list-islist-islist-new-compactness-base

[T:Type]. ∀[t:co-list-islist(T)].  islist(t)


Proof




Definitions occuring in Statement :  co-list-islist: co-list-islist(T) islist: islist(t) uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T islist: islist(t) has-value: (a)↓
Lemmas referenced :  co-list-islist-islist co-list-islist_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalRule axiomSqleEquality isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[t:co-list-islist(T)].    islist(t)



Date html generated: 2016_05_15-PM-10_11_19
Last ObjectModification: 2015_12_27-PM-05_58_17

Theory : eval!all


Home Index