proposition: Lemma rule_ok : forall l r, rule l r -> exists f n (ls : Tes n), l = apps (Fun f) ls.
proof: Proof. intros l r h. ex (lhs_fun h) (lhs_nb_args h) (lhs_args h). apply lhs_ok. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(LogicUtil RelUtil VecOrd VecUtil LAlpha)