---

Step * of Lemma member-dep-isect

∀A:Type. ∀B:A ⟶ Type. ∀x:a:A ⋂ B[a].  (x ∈ B[x])
BY
{ (Auto THEN DepIsectHD (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}x:a:A  \mcap{}  B[a].    (x  \mmember{}  B[x])


By

---

Latex:
(Auto  THEN  DepIsectHD  (-1)  THEN  Auto)

---

Home Index