Using Sozeau's equations to mimick http://researchblogs.cs.bham.ac.uk/thelablunch/2015/09/a-simple-proof-checker-for-teaching/

Append.v

Require Import Equations.
Require Import List.
Require String. Open Scope string_scope.

Ltac Case str :=
  let val := eval compute in (String.append "case " str)
  in idtac val.

Equations append {A : Type} (xs ys : list A) : list A
:= append A []          ys := ys
;  append A (cons x xs) ys := cons x (append xs ys).

Theorem append_neutral :
  forall {A} (xs : list A), append xs nil = xs.
Proof.
induction 0 as [|hd tl].

  - Case "[]".
    assert (H0 : @append A [] [] = [])
      by apply append_equation_1.
    exact H0.

  - Case "hd :: tl".
    assert (H1 : append (hd :: tl) [] = hd :: append tl [])
      by apply append_equation_2.
    assert (H2 : append (hd :: tl) [] = hd :: tl)
      by (rewrite H1, IHtl; trivial).
    exact H2.
Qed.