---

Step * of Lemma append-impossible

∀[T:Type]. ∀[as,bs:T List]. ∀[b:T].  uiff(as = (as @ [b / bs]) ∈ (T List);False)
BY
{ (Auto THEN Assert ⌜(as @ []) = (as @ [b / bs]) ∈ (T List)⌝⋅) }

1
.....assertion..... 
1. T : Type
2. as : T List
3. bs : T List
4. b : T
5. as = (as @ [b / bs]) ∈ (T List)
⊢ (as @ []) = (as @ [b / bs]) ∈ (T List)

2
1. T : Type
2. as : T List
3. bs : T List
4. b : T
5. as = (as @ [b / bs]) ∈ (T List)
6. (as @ []) = (as @ [b / bs]) ∈ (T List)
⊢ False

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}(as  @  [])  =  (as  @  [b  /  bs])\mkleeneclose{}\mcdot{})

---

Home Index