proposition: Lemma eq_apps_fun_nb_args_sym : forall f p (ts : Tes p) g q (us : Tes q), apps (Fun f) ts = apps (Fun g) us -> q = p.
proof: Proof. intros f p ts g q us e. sym. eapply eq_apps_fun_nb_args. apply e. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)