(* Sample solution to the reverse problem *)

(*******************************************************************)

Lemma rev_helper_rev_append : forall l1 l2, rev_helper l1 l2 = rev l1 ++ l2.
  Proof.
    induction l1 as [|n l1'].
    Case "l1 = []".
      reflexivity. 
    Case "l1 = cons n l1'".
      intros l2.
      simpl. rewrite->snoc_append. 
      rewrite <- ass_app. simpl.
      rewrite ->IHl1'. reflexivity.
  Qed.

Theorem rev_rev' : forall l : natlist, rev l = rev' l.
Proof.
  intros l.
  unfold rev'.
  induction l as [|n l'].
  Case "l = nil". reflexivity.
  Case " l = cons n l'".
    simpl. rewrite -> IHl'. rewrite -> snoc_append.
    rewrite <- IHl'.
    rewrite -> rev_helper_rev_append.
    reflexivity.
Qed.

(*******************************************************************)