---

Step * of Lemma cons_cons_permr

No Annotations
∀T:Type. ∀a,a':T. ∀as,as':T List.  ((as ≡(T) as') ⇒ ([a; [a' / as]] ≡(T) [a'; [a / as']]))
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}T:Type.  \mforall{}a,a':T.  \mforall{}as,as':T  List.    ((as  \mequiv{}(T)  as')  {}\mRightarrow{}  ([a;  [a'  /  as]]  \mequiv{}(T)  [a';  [a  /  as']]))


By

---

Latex:
Auto

---

Home Index