proposition: Lemma rev_acc_eq : forall {A} (l : list A), rev_acc l = rev l.
proof: Proof. apply (rev_acc_elim (fun A l revaccl => revaccl = rev l) (fun A _ acc l go_res => go_res = rev l ++ acc)); intros; simpl. + now rewrite app_nil_r in H. + reflexivity. + now rewrite H, <- app_assoc. Qed.
imports: Equations(Equations) Coq(List Program.Syntax Arith Lia)