We want to prove

.L1,L2,L3:List (append(append(L1, L2), L3) = append(L1, append(L2, L3)))

- Base case : prove assertion for
L1 = nil - Quantifier elimination introduces new
constants *l2 l3 :List*. - Show
append(append(nil, l2), l3) = append(nil, append(l2, l3))

- Quantifier elimination introduces new
- Induction case : prove assertion for
L1 = cons(M,L) L1 = L - Quantifier elimination introduces new
constants *m :Nat*and*l :List*. - Implication elimination assumes
L2,L3:List (append(append(l, L2), L3) = append(l, append(L2, L3))) - Change hypothesis
L2,L3:List (append(append(l, L2), L3) = append(l, append(L2, L3))) - Quantifier elimination introduces new
constants *l2 l3 :List*. - Show
append(append(cons(m,l), l2), l3) = append(cons(m,l), append(l2, l3))

- Quantifier elimination introduces new