Definition princop {s: sorts σ} (t: term σ s): names σ := pr1 (term_decompose t).
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Algebra.Universal.SortedTypes.