---

Step * of Lemma l_intersection_wf

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[L1,L2:A List].  (l_intersection(eq;L1;L2) ∈ A List)
BY
{ (Unfold `l_intersection` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[L1,L2:A  List].    (l\_intersection(eq;L1;L2)  \mmember{}  A  List)


By

---

Latex:
(Unfold  `l\_intersection`  0  THEN  Auto)

---

Home Index