---

Step * 1 of Lemma subtype_rel_isect


1. A : Type
2. T : Type
3. B : T ⟶ Type
4. A ⊆r (⋂x:T. B[x])
5. x : T
⊢ A ⊆r B[x]
BY
{ (Using [`B', ⌜⋂x:T. B[x]⌝] (BLemma `subtype_rel_transitivity`)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  T  :  Type
3.  B  :  T  {}\mrightarrow{}  Type
4.  A  \msubseteq{}r  (\mcap{}x:T.  B[x])
5.  x  :  T
\mvdash{}  A  \msubseteq{}r  B[x]


By

---

Latex:
(Using  [`B',  \mkleeneopen{}\mcap{}x:T.  B[x]\mkleeneclose{}]  (BLemma  `subtype\_rel\_transitivity`)\mcdot{}  THEN  Auto)

---

Home Index