proposition: Lemma SameValues_Equal_Ext : forall {av} tenv state m1 m2, @StringMap.Equal (Value av) m1 m2 -> (state ≲ tenv ∪ m1 -> state ≲ tenv ∪ m2).
proof: Proof. induction tenv as [ | ? ? ? IH ]; repeat match goal with | [ H: forall v st m1 m2, StringMap.Equal m1 m2 -> st ≲ ?tail v ∪ m1 -> st ≲ ?tail v ∪ m2, H': StringMap.Equal ?m1 ?m2, H'': ?st ≲ ?tail ?v ∪ (StringMap.add ?k ?v ?m1) |- ?st ≲ ?tail ?v ∪ (StringMap.add ?k ?v ?m2) ] => apply (fun pr => IH v st _ _ pr H'') | [ |- StringMap.Equal (StringMap.add ?k ?v ?m1) (StringMap.add ?k ?v ?m2) ] => solve [eauto using add_m, Equal_refl] | _ => solve [eauto] | _ => t_Morphism_step end. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid