Nuprl Lemma : subtype_rel_ifthenelse
∀[b:𝔹]. ∀[A1,A2,B1,B2:Type].
(if b then A1 else B1 fi ⊆r if b then A2 else B2 fi ) supposing ((A1 ⊆r A2) and (B1 ⊆r B2))
Proof
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
bool: 𝔹,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
bfalse: ff,
prop: ℙ,
subtype_rel: A ⊆r B
Lemmas referenced :
bool_wf,
equal_wf,
subtype_rel_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
hypothesisEquality,
thin,
extract_by_obid,
hypothesis,
lambdaFormation,
sqequalHypSubstitution,
unionElimination,
equalityElimination,
sqequalRule,
isectElimination,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
axiomEquality,
cumulativity,
isect_memberEquality,
because_Cache
Latex:
\mforall{}[b:\mBbbB{}]. \mforall{}[A1,A2,B1,B2:Type].
(if b then A1 else B1 fi \msubseteq{}r if b then A2 else B2 fi ) supposing ((A1 \msubseteq{}r A2) and (B1 \msubseteq{}r B2))
Date html generated:
2018_05_21-PM-00_00_52
Last ObjectModification:
2017_10_10-PM-04_20_10
Theory : union
Home
Index