### Nuprl Lemma : ispair-bool-if-co-list

`∀[T:Type]. ∀[t:colist(T)].  (ispair(t) ∈ 𝔹)`

Proof

Definitions occuring in Statement :  colist: `colist(T)` bfalse: `ff` btrue: `tt` bool: `𝔹` uall: `∀[x:A]. B[x]` ispair: `if z is a pair then a otherwise b` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` or: `P ∨ Q` guard: `{T}` uimplies: `b supposing a` and: `P ∧ Q` unit: `Unit` exists: `∃x:A. B[x]` ext-eq: `A ≡ B`
Lemmas referenced :  colist-ext istype-universe co-list-cases subtype_rel_b-union-left unit_wf2 colist_wf unit_subtype_colist ext-eq_inversion b-union_wf subtype_rel_transitivity subtype_rel_weakening bfalse_wf subtype_rel_b-union-right btrue_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality instantiate universeEquality dependent_functionElimination unionElimination hypothesis_subsumption productEquality independent_isectElimination because_Cache productElimination equalityTransitivity equalitySymmetry equalityElimination sqequalRule axiomEquality universeIsType

Latex:
\mforall{}[T:Type].  \mforall{}[t:colist(T)].    (ispair(t)  \mmember{}  \mBbbB{})

Date html generated: 2019_10_16-AM-11_38_17
Last ObjectModification: 2019_06_26-PM-04_07_03

Theory : eval!all

Home Index