proposition: Lemma WF_hd_red_mod_lab : WF (hd_red_mod E R) <-> WF (hd_red_mod (lab_rules E) (lab_rules R)).
proof: Proof. rewrite WF_hd_red_mod_lab. 2: apply ge_compatE. rewrite Decr_empty, union_empty_l. refl. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)