proposition: Lemma iter_fp {A} (f : A -> A) x : f x = x -> forall n, iterate f n x = x.
proof: Proof. intros E. induction n. reflexivity. now rewrite iterate_S, IHn. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics Autosubst_Lemmas