proposition: Lemma rev_rev_acc : forall {A} (l : list A), rev_acc l [] = rev l.
proof: Proof. intros. myreplace (rev l) with (rev l +++ []) by (symmetry; apply app'_nil). generalize (@Datatypes.nil A). funelim (rev l). - intros. reflexivity. - intros l'. autorewrite with rev_acc. rewrite X. rewrite app'_assoc. reflexivity. Qed.
imports: Equations(CoreTactics) Equations.HoTT.All Equations.HoTT.WellFounded Coq.Unicode.Utf8 HoTT.Types.Bool HoTT.Spaces.Nat HoTT.Classes.implementations.peano_naturals Equations.HoTT.Tactics