proposition: Lemma SameValues_Equal : forall {av} tenv m1 m2 ext, @StringMap.Equal (Value av) m1 m2 -> (m1 ≲ tenv ∪ ext -> m2 ≲ tenv ∪ ext).
proof: Proof. induction tenv; repeat match goal with | [ IH: _, H: StringMap.remove ?k ?m1 ≲ (?t ?v) ∪ ?ext, H': StringMap.Equal ?m1 ?m2 |- StringMap.remove ?k ?m2 ≲ (?t ?v) ∪ ?ext ] => apply (IH _ _ _ _ (remove_m eq_refl H')); exact H | _ => solve [eauto] | _ => t_Morphism_step end. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid