proposition: Lemma TelStrongEq_trans {A} : Transitive (@TelStrongEq A).
proof: Proof. red; intros tel; induction tel; TelStrongEq_morphism_t. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.Core CertifiedExtraction.Utils Coq.Setoids.Setoid Eqdep