---

Step * of Lemma append-impossible2

∀[T:Type]. ∀[as,bs,cs:T List].  ∀[b:T]. uiff(cs = (as @ [b / bs]) ∈ (T List);False) supposing cs ≤ as
BY
{ (((((((Auto THEN (FLemma `iseg_length` [(-3)])) THENA Auto) THEN (HypSubst (-2) (-1))) THENA Auto)
     THEN (RWO "length_append" (-1))
     )
    THENA Auto
    )
   THEN (Reduce (-1))
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs,cs:T  List].    \mforall{}[b:T].  uiff(cs  =  (as  @  [b  /  bs]);False)  supposing  cs  \mleq{}  as


By

---

Latex:
(((((((Auto  THEN  (FLemma  `iseg\_length`  [(-3)]))  THENA  Auto)  THEN  (HypSubst  (-2)  (-1)))  THENA  Auto)
      THEN  (RWO  "length\_append"  (-1))
      )
    THENA  Auto
    )
  THEN  (Reduce  (-1))
  THEN  Auto')

---

Home Index