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