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