proposition: Lemma rev_app' : forall {A} (l l' : list A), rev (l +++ l') = rev l' +++ rev l.
proof: Proof. intros. funelim (l +++ l'); simp rev app'; trivial. now (rewrite X, <- app'_assoc). 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