proposition: Lemma is_notvar_rhs_false : forall R, forallb is_notvar_rhs R = true -> forall x l, In (mkRule l (Var x)) R -> False.
proof: Proof. intros. rewrite forallb_forall in H. ded (H _ H0). discr. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)