proposition: Lemma SameSCAs_remove: forall (av : Type) (m1 m2 : StringMap.t (Value av)) (k : StringMap.key), SameSCAs m2 m1 -> SameSCAs (StringMap.remove k m2) (StringMap.remove k m1).
proof: Proof. unfold SameSCAs; t_Same. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid