---

Step * of Lemma dep-isect-subtype2

∀[A1,A2:Type]. ∀[B1:A1 ⟶ Type]. ∀[B2:A2 ⟶ Type].
  (x:A1 ⋂ B1[x] ⊆r x:A2 ⋂ B2[x]) supposing ((∀x:A1. (B1[x] ⊆r B2[x])) and (A1 ⊆r A2))
BY
{ (Auto THEN (D 0 THENA Auto) THEN DepIsectHD (-1) THEN DepIsectCD THEN Auto THEN DoSubsume THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A1,A2:Type].  \mforall{}[B1:A1  {}\mrightarrow{}  Type].  \mforall{}[B2:A2  {}\mrightarrow{}  Type].
    (x:A1  \mcap{}  B1[x]  \msubseteq{}r  x:A2  \mcap{}  B2[x])  supposing  ((\mforall{}x:A1.  (B1[x]  \msubseteq{}r  B2[x]))  and  (A1  \msubseteq{}r  A2))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  DepIsectHD  (-1)  THEN  DepIsectCD  THEN  Auto  THEN  DoSubsume  THEN  Auto)

---

Home Index