---

Step * 1 of Lemma compat-append


1. [T] : Type
⊢ ∀cs,bs,ds:T List.  ([] @ bs || cs @ ds ⇒ [] || cs)
BY
{ (Auto THEN Unfold `compat` 0 THEN OrLeft THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  \mforall{}cs,bs,ds:T  List.    ([]  @  bs  ||  cs  @  ds  {}\mRightarrow{}  []  ||  cs)


By

---

Latex:
(Auto  THEN  Unfold  `compat`  0  THEN  OrLeft  THEN  Auto)

---

Home Index