proposition: Lemma ProgOk_Chomp_None : forall {av A} env value prog (tail1: A -> Telescope av) (tail2: A -> Telescope av) ext, (forall v, value ↝ v -> {{ tail1 v }} prog {{ tail2 v }} ∪ {{ ext }} // env) -> ({{ Cons NTNone value tail1 }} prog {{ Cons NTNone value tail2 }} ∪ {{ ext }} // env).
proof: Proof. repeat match goal with | _ => SameValues_Facade_t_step | _ => progress SameValues_Fiat_t | [ H: forall v, ?val ↝ v -> _, H': ?val ↝ ?v |- _ ] => learn (H _ H') end. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas