proposition: Lemma dup_hd_rules_graph_incl_hde : hd_rules_graph (red R #) D << hde D.
proof: Proof. unfold inclusion. intros. apply (@int_red_hd_rules_graph_incl_hde _ R D x y). destruct H. decomp H0. rewrite forallb_forall in hd_hyp. ded (hd_hyp _ H). compute in H0. destruct x. destruct rhs. discr. destruct f. unfold hd_rules_graph. intuition. exists x0. exists x1. simpl rhs. rewrite sub_fun. apply dup_int_rules_int_red_rtc; hyp. discr. Qed.
imports: CoLoR(ADecomp ADuplicateSymb ATrs ListUtil RelSub RelUtil AGraph LogicUtil BoolUtil AShift EqUtil ListDec)