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