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