proposition: Theorem app_assoc : forall (lst1 lst2 lst3 : natlist), (lst1 ++ lst2) ++ lst3 = lst1 ++ (lst2 ++ lst3).
proof: Proof. intros lst1 lst2 lst3. induction lst1 as [| h1 t1]. - reflexivity. - simpl. rewrite -> IHt1. reflexivity. Qed.