proposition: Lemma is_notvar_rhs_elim : forall R, forallb is_notvar_rhs R = true -> forall l r, In (mkRule l r) R -> exists f ts, r = Fun f ts.
proof: Proof. intros. rewrite forallb_forall in H. ded (H _ H0). destruct r. discr. ex f t. refl. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)