---

Step * of Lemma list-equal-subsume

∀[A,B:Type]. ∀[x,y:A List].  {x = y ∈ (B List) supposing x = y ∈ (A List)} supposing {a:A| (a ∈ x)}  ⊆r B
BY
{ (Unfold `guard` 0 THEN Auto THEN SubsumeC {a:A| (a ∈ x)}  List⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[x,y:A  List].    \{x  =  y  supposing  x  =  y\}  supposing  \{a:A|  (a  \mmember{}  x)\}    \msubseteq{}r  B


By

---

Latex:
(Unfold  `guard`  0  THEN  Auto  THEN  SubsumeC  \{a:A|  (a  \mmember{}  x)\}    List\mcdot{}  THEN  Auto)

---

Home Index