---

Step * 2 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 C
BY
{ ((InstHyp [⌜ff⌝] (-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  C


By

---

Latex:
((InstHyp  [\mkleeneopen{}ff\mkleeneclose{}]  (-1)\mcdot{}  THENM  Reduce  (-1))  THEN  Auto)\mcdot{}

---

Home Index