proposition: Lemma TelStrongEq_Stronger : forall {A} ext tenv tenv', @TelStrongEq A tenv tenv' -> TelEq ext tenv tenv'.
proof: Proof. induction tenv; destruct tenv'; repeat match goal with | _ => cleanup | _ => TelStrongEq_t | _ => SameValues_Fiat_t end. reflexivity. rewrite <- H3. apply TelEq_chomp_head; red; intros; eauto. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas