proposition: Lemma map_last_sym : forall (A B : Type) (f : A -> B) (a : A) (l : list A), @app _ (@map A B f l) (@cons _ (f a) (@nil _)) = @map _ _ f (@app A l (@cons _ a (@nil _))).
proof: Proof. intros. autoinduct on map || (idtac "step1 test7 fails (many arguments)"; induction l). all: (simpl; congruence). Qed.
imports: Autoinduct(Autoinduct)