---

Step * of Lemma l_subset_right_cons_trivial

∀[T:Type]. ∀x:T. ∀L:T List.  l_subset(T;L;[x / L])
BY
{ (Unfold `l_subset` 0 THEN Auto THEN GenListD 0 THEN OrRight THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}L:T  List.    l\_subset(T;L;[x  /  L])


By

---

Latex:
(Unfold  `l\_subset`  0  THEN  Auto  THEN  GenListD  0  THEN  OrRight  THEN  Auto)

---

Home Index