proposition: Lemma ProgOk_Chomp_Some : forall `{FacadeWrapper (Value av) A} env key value prog (tail1: A -> Telescope av) (tail2: A -> Telescope av) ext, key ∉ ext -> (forall v: A, value ↝ v -> {{ tail1 v }} prog {{ tail2 v }} ∪ {{ [key |> wrap v] :: ext }} // env) -> ({{ Cons (NTSome key) value tail1 }} prog {{ Cons (NTSome key) value tail2 }} ∪ {{ ext }} // env).
proof: Proof. intros; apply ProkOk_specialize_to_ret; intros; apply ProgOk_Chomp_lemma; eauto. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas