proposition: Lemma nb_args_apps : forall n (ts : Tes n) t, nb_args (apps t ts) = nb_args t + n.
proof: Proof. induction ts; intro t; simpl. lia. rewrite IHts. simpl. lia. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)