---

Step * of Lemma list_eq_imp_sqeq

∀T:Type. ∀L1,L2:T List.  ((L1 = L2 ∈ (T List)) ⇒ (L1 ~ L2)) supposing T ⊆r Base
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}L1,L2:T  List.    ((L1  =  L2)  {}\mRightarrow{}  (L1  \msim{}  L2))  supposing  T  \msubseteq{}r  Base


By

---

Latex:
Auto

---

Home Index