---

Step * of 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))
BY
{ Auto }

---

Latex:

---

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))


By

---

Latex:
Auto

---

Home Index