Step
*
1
of Lemma
subtype_rel_isect2
1. A : Type
2. B : Type
3. C : Type
4. ∀[b:𝔹]. (A ⊆r if b then B else C fi )
⊢ A ⊆r B
BY
{ ((InstHyp [⌜tt⌝] (-1)⋅ THENM Reduce (-1)) THEN Auto)⋅ }
Latex:
Latex:
1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  \mforall{}[b:\mBbbB{}].  (A  \msubseteq{}r  if  b  then  B  else  C  fi  )
\mvdash{}  A  \msubseteq{}r  B
By
Latex:
((InstHyp  [\mkleeneopen{}tt\mkleeneclose{}]  (-1)\mcdot{}  THENM  Reduce  (-1))  THEN  Auto)\mcdot{}
Home
Index