proposition: Lemma SameADTs_impl {av} {m1 m2} : SameADTs m1 m2 -> (forall k v, StringMap.MapsTo k (@ADT av v) m1 -> StringMap.MapsTo k (@ADT av v) m2).
proof: Proof. unfold SameADTs; firstorder. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid