---

Step * of Lemma compat_symmetry

∀[T:Type]. ∀as,bs:T List.  (as || bs ⇐⇒ bs || as)
BY
{ (Unfold `compat` 0
   THEN Auto
   THEN SplitOrHyps
   THEN ((OrLeft THEN Complete (Auto)) ORELSE (OrRight THEN Complete (Auto)))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}as,bs:T  List.    (as  ||  bs  \mLeftarrow{}{}\mRightarrow{}  bs  ||  as)


By

---

Latex:
(Unfold  `compat`  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  ((OrLeft  THEN  Complete  (Auto))  ORELSE  (OrRight  THEN  Complete  (Auto))))

---

Home Index