Nuprl Lemma : colist-cases
∀[T:Type]. ∀x:colist(T). ((x ~ Ax) ∨ (x ∈ T × colist(T)))
Proof
Definitions occuring in Statement :
colist: colist(T),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
or: P ∨ Q,
member: t ∈ T,
product: x:A × B[x],
universe: Type,
sqequal: s ~ t,
axiom: Ax
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
ext-eq: A ≡ B,
and: P ∧ Q,
all: ∀x:A. B[x],
subtype_rel: A ⊆r B,
b-union: A ⋃ B,
tunion: ⋃x:A.B[x],
bool: 𝔹,
unit: Unit,
ifthenelse: if b then t else f fi ,
pi2: snd(t),
bfalse: ff,
btrue: tt,
it: ⋅,
or: P ∨ Q,
top: Top
Lemmas referenced :
colist-ext,
colist_wf,
pair-sq-axiom-wf,
istype-void
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
productElimination,
Error :lambdaFormation_alt,
hypothesis_subsumption,
applyEquality,
sqequalRule,
imageElimination,
unionElimination,
equalityElimination,
Error :inlEquality_alt,
axiomSqEquality,
Error :equalityIsType4,
Error :productIsType,
Error :universeIsType,
because_Cache,
baseClosed,
Error :inrEquality_alt,
axiomEquality,
independent_pairEquality,
universeEquality,
Error :isect_memberEquality_alt,
voidElimination,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[T:Type]. \mforall{}x:colist(T). ((x \msim{} Ax) \mvee{} (x \mmember{} T \mtimes{} colist(T)))
Date html generated:
2019_06_20-PM-00_38_32
Last ObjectModification:
2018_10_03-PM-01_54_27
Theory : list_0
Home
Index