proposition: Lemma term_extens {s: sorts σ} {t1 t2 : term σ s} (p : term2oplist t1 = term2oplist t2) : t1 = t2.
proof: Proof. apply subtypePairEquality'. 2: apply isapropisaterm. assumption. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.Combinatorics.Maybe UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Signatures