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