fact: Fixpoint term_size {a : nat} {tys : Vector.t obj_pair a} {dom cod} (t : @Term a tys dom cod) : nat := match t with | Ident => 1%nat | Morph _ => 1%nat | Comp f g => 1%nat + term_size f + term_size g end.
imports: Coq.Vectors.Vector Coq.PArith.PArith Lia Equations.Prop.Equations Wellfounded Relations