proposition: Lemma SameValues_WeakEq_Ext : forall {av} tenv state m1 m2, @WeakEq av m2 m1 -> (state ≲ tenv ∪ m1 -> state ≲ tenv ∪ m2).
proof: Proof. induction tenv as [ | ? ? ? IH ]; repeat match goal with | _ => t_Morphism_step | _ => solve [eauto using WeakEq_Trans] end. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid