proposition: Lemma SameValues_MapsTo_Ext_State: forall {av : Type} {tel: Telescope av} (key : StringMap.key) {ext st : StringMap.t (Value av)}, st ≲ tel ∪ ext -> forall v, StringMap.MapsTo key v ext -> StringMap.MapsTo key v st.
proof: Proof. induction tel; repeat match goal with | _ => progress intros | _ => tauto | [ H: ?a /\ ?b |- _ ] => destruct H | [ H: _ ≲ Nil ∪ _ |- _ ] => simpl in H | [ H: StringMap.Equal ?b ?a, H': StringMap.MapsTo ?k _ _ |- StringMap.MapsTo ?k _ _ ] => rewrite H | [ H: ?st ≲ Cons ?key ?val ?tail ∪ ?ext |- _ ] => simpl in H; destruct key | [ H: forall a key ext st, st ≲ ?tail a ∪ ext -> _, H': ?st ≲ ?tail ?v ∪ ?ext, H'': StringMap.MapsTo ?key ?v' _ |- _ ] => specialize (H v key ext st H' v' H''); rename H into IHREC | [ H: StringMap.MapsTo ?k ?v (StringMap.remove _ ?s) |- StringMap.MapsTo ?k ?v ?s ] => solve[eauto using MapsTo_remove] | [ H: match StringMap.find ?s ?st with _ => _ end |- _ ] => let a := fresh in destruct (StringMap.find s st) eqn:a | [ H: exists v, _ |- _ ] => destruct H end; eauto using WeakEq_Mapsto_MapsTo. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid