proposition: Lemma red_rule_top : forall l r s, In (mkRule l r) R -> red R (sub s l) (sub s r).
proof: Proof. intros. unfold red. ex l r (@Hole Sig) s. auto. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)