Definition make_term {σ: signature} {s: sorts σ} {l: oplist σ} (lstack: isaterm s l) : term σ s := l ,, lstack.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Algebra.Universal.SortedTypes.