proposition: Theorem rev_length : forall l : natlist, length (rev l) = length l.
proof: Proof. MProof. intros l. elim l &> [i: ~~| \n l' IHl']. - reflexivity. - simpl. rewrite -> app_length, plus_comm. simpl. rewrite -> IHl'. reflexivity. Qed.