Nuprl Lemma : respects-equality-union
∀[T1,T2,S1,S2:Type]. (respects-equality(S1;T1) ⇒ respects-equality(S2;T2) ⇒ respects-equality(S1 + S2;T1 + T2))
Proof
Definitions occuring in Statement :
respects-equality: respects-equality(S;T),
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
union: left + right,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
respects-equality: respects-equality(S;T),
all: ∀x:A. B[x],
member: t ∈ T,
subtype_rel: A ⊆r B,
guard: {T},
uimplies: b supposing a,
top: Top,
or: P ∨ Q,
and: P ∧ Q,
cand: A c∧ B,
outl: outl(x),
isl: isl(x),
assert: ↑b,
ifthenelse: if b then t else f fi ,
bfalse: ff,
sq_type: SQType(T),
true: True,
false: False,
outr: outr(x),
bnot: ¬bb,
btrue: tt
Lemmas referenced :
union-eta,
subtype_rel_union,
top_wf,
istype-void,
outl_wf,
subtype_base_sq,
int_subtype_base,
subtype_rel-equal,
equal_functionality_wrt_subtype_rel2,
outr_wf,
istype-base,
respects-equality_wf,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
Error :lambdaFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
equalityTransitivity,
hypothesis,
equalitySymmetry,
applyEquality,
isectElimination,
hypothesisEquality,
because_Cache,
independent_isectElimination,
Error :lambdaEquality_alt,
Error :isect_memberEquality_alt,
voidElimination,
Error :universeIsType,
sqequalRule,
unionElimination,
Error :inlEquality_alt,
Error :dependent_set_memberEquality_alt,
independent_pairFormation,
Error :productIsType,
Error :equalityIstype,
baseApply,
closedConclusion,
baseClosed,
sqequalBase,
applyLambdaEquality,
setElimination,
rename,
productElimination,
promote_hyp,
natural_numberEquality,
instantiate,
cumulativity,
intEquality,
independent_functionElimination,
unionEquality,
Error :inrEquality_alt,
Error :unionIsType,
Error :inhabitedIsType,
universeEquality
Latex:
\mforall{}[T1,T2,S1,S2:Type].
(respects-equality(S1;T1) {}\mRightarrow{} respects-equality(S2;T2) {}\mRightarrow{} respects-equality(S1 + S2;T1 + T2))
Date html generated:
2019_06_20-AM-11_20_02
Last ObjectModification:
2018_11_23-PM-02_15_26
Theory : union
Home
Index