---

Step * of Lemma l_contains_append

∀[T:Type]. ∀A,B:T List.  A ⊆ A @ B
BY
{ (Intros
   THEN Unfold `l_contains` 0
   THEN (RWO "l_all_iff" 0 THENA Auto)
   THEN RWO "member_append" 0
   THEN Auto
   THEN OrLeft
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}A,B:T  List.    A  \msubseteq{}  A  @  B


By

---

Latex:
(Intros
  THEN  Unfold  `l\_contains`  0
  THEN  (RWO  "l\_all\_iff"  0  THENA  Auto)
  THEN  RWO  "member\_append"  0
  THEN  Auto
  THEN  OrLeft
  THEN  Auto)

---

Home Index