proposition: Lemma app'_nil : forall {A : Type} (l : list A), l +++ [] = l.
proof: Proof. intros. funelim (app' l []); auto. now rewrite X. 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