proposition: Lemma TelEq_chomp_head : forall {av A} k v ext tenv tenv', @PointWise_TelEq av A ext v tenv tenv' -> TelEq ext (Cons k v tenv) (Cons k v tenv').
proof: Proof. intros * H; rewrite H; reflexivity. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas