proposition: Lemma red_ren : forall R, red R << red (map (sub_rule s2) R).
proof: Proof. intros R t u h. redtac. subst. rewrite <- (sub_inv hyp l), <- (sub_inv hyp r), sub_sub, sub_sub with (s1:=s) (s2:=s1). apply red_rule. change (In (sub_rule s2 (mkRule l r)) (map (sub_rule s2) R)). apply in_map. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)