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