proposition: Lemma eq_apps_nb_args_args : forall n (ts us : Tes n) t u, apps t ts = apps u us -> ts = us.
proof: Proof. induction ts; simpl; intros us t u. VOtac. refl. VSntac us. simpl. intro e. gen (eq_apps_nb_args_head e); intro i. inversion i. subst t h; clear i. apply Vtail_eq. eapply IHts. apply e. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)