---

Step * of Lemma cons-l_contains

∀[T:Type]. ∀A,B:T List. ∀x:T.  (A ⊆ B ⇒ A ⊆ [x / B])
BY
{ (InstLemma `l_contains-append4` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Auto
   THEN (InstHyp [⌜[x]⌝;⌜B⌝] (-4)⋅ THENA Auto)
   THEN Reduce (-1)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}A,B:T  List.  \mforall{}x:T.    (A  \msubseteq{}  B  {}\mRightarrow{}  A  \msubseteq{}  [x  /  B])


By

---

Latex:
(InstLemma  `l\_contains-append4`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}[x]\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Trivial)

---

Home Index