proposition: Fact Forall_rev X (P : X -> Prop) ll : Forall P ll -> Forall P (rev ll).
proof: Proof. induction 1 as [ | x ll Hll IH ]. constructor. simpl. apply Forall_app; split; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)