Nuprl Lemma : co-list-cases2
∀[T:Type]. ∀x:colist(T). ((x = Ax ∈ colist(T)) ∨ (∃t:T. ∃y:colist(T). (x = <t, y> ∈ colist(T))))
Proof
Definitions occuring in Statement :
colist: colist(T),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
or: P ∨ Q,
pair: <a, b>,
universe: Type,
equal: s = t ∈ T,
axiom: Ax
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
member: t ∈ T,
ext-eq: A ≡ B,
and: P ∧ Q,
subtype_rel: A ⊆r B,
implies: P ⇒ Q,
b-union: A ⋃ B,
tunion: ⋃x:A.B[x],
bool: 𝔹,
unit: Unit,
ifthenelse: if b then t else f fi ,
pi2: snd(t),
or: P ∨ Q,
it: ⋅,
guard: {T},
uimplies: b supposing a,
exists: ∃x:A. B[x],
respects-equality: respects-equality(S;T)
Lemmas referenced :
colist-ext,
subtype_rel_b-union-right,
unit_wf2,
colist_wf,
it_wf,
subtype_rel_b-union-left,
unit_subtype_colist,
subtype_rel_transitivity,
b-union_wf,
co-list-subtype,
subtype-respects-equality,
product_subtype_colist,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
productElimination,
lambdaEquality_alt,
applyEquality,
hypothesis,
productEquality,
sqequalRule,
productIsType,
universeIsType,
because_Cache,
inhabitedIsType,
imageElimination,
unionElimination,
equalityElimination,
inlEquality_alt,
axiomEquality,
independent_isectElimination,
equalityIstype,
baseClosed,
independent_pairEquality,
sqequalBase,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
inrEquality_alt,
dependent_pairEquality_alt,
equalityTransitivity,
instantiate,
universeEquality
Latex:
\mforall{}[T:Type]. \mforall{}x:colist(T). ((x = Ax) \mvee{} (\mexists{}t:T. \mexists{}y:colist(T). (x = <t, y>)))
Date html generated:
2020_05_20-AM-09_07_47
Last ObjectModification:
2019_12_31-PM-07_06_24
Theory : eval!all
Home
Index