Nuprl Lemma : per-union-elim
∀[A,B:Type].
∀x:per-union(A;B)
per-or(uand(x ~ inl outl(x);outl(x) ∈ A supposing x ~ inl outl(x));uand(x ~ inr outr(x) ;outr(x) ∈ B
supposing x
~ inr outr(x) ))
Proof
Definitions occuring in Statement :
per-union: per-union(A;B),
per-or: per-or(A;B),
uand: uand(A;B),
outr: outr(x),
outl: outl(x),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
member: t ∈ T,
inr: inr x ,
inl: inl x,
universe: Type,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
member: t ∈ T,
per-or: per-or(A;B),
per-exists: per-exists(A;a.B[a]),
so_lambda: λ2x.t[x],
so_apply: x[s],
uand: uand(A;B),
has-value: (a)↓,
top: Top,
per-function: per-function(A;a.B[a]),
function-eq: function-eq(A;a.B[a];f;g),
uimplies: b supposing a,
subtype_rel: A ⊆r B,
sq_type: SQType(T),
implies: P ⇒ Q,
guard: {T},
squash: ↓T,
prop: ℙ,
true: True,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
per-union: per-union(A;B),
outl: outl(x),
outr: outr(x),
false: False
Lemmas referenced :
per-union-elim1,
per-product-elim,
per-value_wf,
has-value_wf_base,
is-exception_wf,
per-value-property,
istype-top,
istype-void,
per-union_wf,
istype-universe,
per-function_wf_type,
per-value_subtype_base,
subtype_base_sq,
base_wf,
subtype_rel_self,
per-union-implies-wf1,
equal_wf,
squash_wf,
true_wf,
iff_weakening_equal,
per-union-implies-wf2,
if-per-void,
uand_wf,
equal-wf-base,
per-void_wf,
member_wf,
member-per-or-left,
int_subtype_base,
istype-base,
member-per-or-right
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
Error :lambdaFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
dependent_functionElimination,
hypothesis,
sqequalRule,
baseClosed,
axiomSqleEquality,
divergentSqle,
sqleReflexivity,
because_Cache,
isaxiomCases,
promote_hyp,
axiomSqEquality,
Error :inhabitedIsType,
Error :isect_memberEquality_alt,
Error :isectIsTypeImplies,
voidElimination,
Error :universeIsType,
instantiate,
universeEquality,
pointwiseFunctionalityForEquality,
equalityTransitivity,
equalitySymmetry,
pertypeMemberEquality,
Error :equalityIstype,
sqequalBase,
axiomEquality,
baseApply,
closedConclusion,
applyEquality,
cumulativity,
independent_isectElimination,
independent_functionElimination,
functionExtensionality,
Error :lambdaEquality_alt,
imageElimination,
natural_numberEquality,
imageMemberEquality,
productElimination,
pointwiseFunctionality,
pertypeElimination,
isinlCases,
rename,
isectEquality,
isinrCases,
intEquality
Latex:
\mforall{}[A,B:Type].
\mforall{}x:per-union(A;B)
per-or(uand(x \msim{} inl outl(x);outl(x) \mmember{} A supposing x \msim{} inl outl(x));uand(x
\msim{} inr outr(x) ;outr(x) \mmember{} B supposing x \msim{} inr outr(x) ))
Date html generated:
2019_06_20-AM-11_30_51
Last ObjectModification:
2019_01_22-AM-09_59_22
Theory : per!type
Home
Index