proposition: Lemma SameValues_Equal_Ext_iff : forall {av} tenv state m1 m2, @StringMap.Equal (Value av) m1 m2 -> (state ≲ tenv ∪ m1 <-> state ≲ tenv ∪ m2).
proof: Proof. intros * H; split; [ | symmetry in H ]; eauto using SameValues_Equal_Ext. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid