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