proposition: Theorem app_assoc : forall l1 l2 l3 : natlist, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
proof: Proof. MProof. intros l1 l2 l3. elim l1 &> [i:~~| \n l1' IHl1']. - reflexivity. - simpl. rewrite -> IHl1'. reflexivity. Qed.