---

Step * of Lemma l_subset_cons_same

∀[T:Type]. ∀x:T. ∀L1,L2:T List.  (l_subset(T;L1;L2) ⇒ l_subset(T;[x / L1];[x / L2]))
BY
{ (Auto THEN BLemma `l_subset_cons` THEN Auto) }

1
1. [T] : Type
2. x : T@i
3. L1 : T List@i
4. L2 : T List@i
5. l_subset(T;L1;L2)@i
6. (x ∈ [x / L2])
⊢ l_subset(T;L1;[x / L2])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}L1,L2:T  List.    (l\_subset(T;L1;L2)  {}\mRightarrow{}  l\_subset(T;[x  /  L1];[x  /  L2]))


By

---

Latex:
(Auto  THEN  BLemma  `l\_subset\_cons`  THEN  Auto)

---

Home Index