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