proposition: Theorem term_ind (P: ∏ (s: sorts σ), term σ s → UU) (R: term_ind_HP P) {s: sorts σ} (t: term σ s) : P s t.
proof: Proof. exact (term_ind_onlength P R (length t) s t (isreflnatleh _)). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.Combinatorics.Maybe UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Signatures