proposition: Lemma map_id_list (g: X -> X) A: (forall x, x ∈ A -> g x = x) -> map g A = A.
proof: Proof. intros. induction A; cbn in *; eauto. rewrite H; intuition idtac. rewrite IHA; firstorder. Qed.
imports: List Arith Lia Morphisms FinFun Init.Wf Undecidability.HOU(std.decidable)