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