proposition: Lemma lhs_nb_args_eq : forall f n (ts : Tes n) r (h : rule (apps (Fun f) ts) r), lhs_nb_args h = n.
proof: Proof. intros f n ts r h. sym. eapply eq_apps_fun_nb_args with (F:=F) (X:=X). apply lhs_ok. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(LogicUtil RelUtil VecOrd VecUtil LAlpha)