proposition: Theorem length_rev : forall {A:Type} (l:list A), length l = length (rev l).
proof: Proof. simple induction l; auto. - intros a l' H; simpl in |- *. rewrite length_app. simpl in |- *; rewrite <- plus_n_Sm; rewrite H; auto with arith. Qed.
imports: List Arith