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