proposition: Lemma lem_itrev {A} : forall lst acc : list A, itrev lst acc = itrev lst [] ++ acc.
proof: Proof. induction lst as [| h t IH]. - auto. - assert (H: itrev t [h] = itrev t [] ++ [h]). { rewrite IH; reflexivity. } sauto db: slist. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation