---

Step * of Lemma isect_subtype_rel_trivial

∀[A,C:Type]. ∀[B:A ⟶ Type].  (⋂x:A. B[x]) ⊆r C supposing ∃x:A. (B[x] ⊆r C)
BY
{ (Auto THEN D 0 THEN Auto THEN (ExRepD THEN SubsumeC ⌜B[x1]⌝⋅) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,C:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    (\mcap{}x:A.  B[x])  \msubseteq{}r  C  supposing  \mexists{}x:A.  (B[x]  \msubseteq{}r  C)


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  (ExRepD  THEN  SubsumeC  \mkleeneopen{}B[x1]\mkleeneclose{}\mcdot{})  THEN  Auto)

---

Home Index