---

Step * 1 of Lemma compat-append2


1. [T] : Type
⊢ ∀cs,bs,ds:T List.  ([] @ bs || cs @ ds ⇒ bs || ds supposing [] = cs ∈ (T List))
BY
{ xxx(((Auto THEN (RevHypSubst (-1) (-2))) THENM (Reduce (-2))) THEN Auto)xxx }

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(((Auto  THEN  (RevHypSubst  (-1)  (-2)))  THENM  (Reduce  (-2)))  THEN  Auto)xxx

---

Home Index