proposition: Lemma red_g : forall a b, red R a b -> red R (g a) (g b).
proof: Proof. intros. apply red_fill. apply red_sub. hyp. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(LogicUtil ATrs ListUtil RelUtil AMatching ListDec APosition NatUtil)