Lemma build_term_inj (nm1 nm2: names σ) (v1: (term σ)⋆ (arity nm1)) (v2: (term σ)⋆ (arity nm2)) (p: sort nm1 = sort nm2) : p # build_term nm1 v1 = build_term nm2 v2 → ∑ eqnm: nm1 = nm2, (transportf (λ op, (term σ)⋆ (arity op)) eqnm v1) = v2. Proof. intro X. set (Y := transportf_total2_const _ _ (λ t s, isaterm s t) _ _ _ p (oplist_build_isaterm nm1 v1)). apply (pathscomp0 (!Y)) in X. clear Y. unfold build_term in X. unfold oplist_build in X. apply (maponpaths pr1) in X. simpl in X. pose (eqnm := X). apply cons_inj1 in eqnm. exists eqnm. induction eqnm. apply cons_inj2 in X. apply vecoplist2oplist_inj in X. exact X. Defined.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Algebra.Universal.SortedTypes.