proposition: Lemma red_mod_g : forall a b, red_mod E R a b -> red_mod E R (g a) (g b).
proof: Proof. intros. apply red_mod_fill. apply red_mod_sub. hyp. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(ATrs LogicUtil ALoop ListUtil RelUtil NatUtil APosition AMatching ARelation)