proposition: Lemma eq_apps_nb_args_sym : forall p (ts : Tes p) q (us : Tes q) a b, apps a ts = apps b us -> nb_args a = nb_args b -> q = p.
proof: Proof. intros p ts q us a b e. sym. eapply eq_apps_nb_args. apply e. hyp. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)