proposition: Lemma mmap_id_ext {A B} {inst : MMap A B} `{@MMapLemmas A B inst} `{@MMapExt A B inst} (f : A -> A) (b : B) : (forall x, f x = x) -> mmap f b = b.
proof: Proof. intros E. rewrite (mmap_ext E). apply mmap_id. Defined.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics Autosubst_Lemmas