proposition: Lemma ProkOk_specialize_to_ret : forall `{FacadeWrapper (Value av) A} env key value prog (tail1: A -> Telescope av) (tail2: A -> Telescope av) ext, (forall v, value ↝ v -> {{ Cons (NTSome key) (ret v) tail1 }} prog {{ Cons (NTSome key) (ret v) tail2 }} ∪ {{ ext }} // env) -> ({{ Cons (NTSome key) value tail1 }} prog {{ Cons (NTSome key) value tail2 }} ∪ {{ ext }} // env).
proof: Proof. repeat match goal with | _ => progress intros | [ |- ?a /\ ?b] => split | [ H: ?a /\ ?b |- _ ] => destruct H | [ |- context[@ProgOk] ] => let h := fresh "init_equiv" in intros ? h; destruct (SameValues_MapsTo_ret_ex _ _ _ _ _ h) as (? & ? & ?) | [ H: ?st ≲ _ ∪ _, H': forall v, ?val ↝ v -> _, H'': ?val ↝ ?x |- _ ] => progress (destruct (H' x H'' st H); deduplicate) | _ => intuition eauto using SameValues_MapsTo_ret_inv end. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid