proposition: Lemma TelEq_chomp_None_left : forall {av A} v ext tenv tenv', (exists vv, v ↝ vv) -> @PointWise_TelEq av A ext v tenv (fun _ => tenv') -> TelEq ext (Cons NTNone v tenv) tenv'.
proof: Proof. intros * ? H; rewrite H; red. split; eauto with SameValues_db. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas