proposition: Lemma hde_bool_correct : hd_rules_graph (int_red R #) D << Graph (hde_bool D).
proof: Proof. incl_trans (hde D). apply int_red_hd_rules_graph_incl_hde. intros x y. rewrite hde_bool_correct_aux. auto. Qed.
imports: CoLoR(ADecomp ADuplicateSymb ATrs ListUtil RelSub RelUtil AGraph LogicUtil BoolUtil AShift EqUtil ListDec)