proposition: Lemma ge_compat : forall l r, In (mkRule l r) R -> l >=I r.
proof: Proof. intros. apply bge_ok. unfold rel. change (brule bge (mkRule l r) = true). rewrite forallb_forall in bge_compat. apply bge_compat. hyp. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)