proposition: Lemma hde_bool_mark_correct : hd_rules_graph (red (dup_int_rules R) #) (dup_hd_rules D) << Graph (hde_bool (dup_hd_rules D)).
proof: Proof. incl_trans (hde (dup_hd_rules D)). 2:{ intros x y. rewrite hde_bool_correct_aux. auto. } intros x y h. destruct h. decomp H0. unfold hde. intuition. destruct (in_map_elim H). destruct H0. destruct x2. unfold dup_hd_rule in H3. simpl in H3. subst x. simpl in *. destruct (in_map_elim H1). destruct H3. destruct x. unfold dup_hd_rule in H4. simpl in H4. subst y. simpl in *. destruct rhs; simpl. trivial. destruct lhs0; simpl. trivial. simpl dup_hd_term in H2. unfold shift in H2. rewrite !sub_fun in H2. destruct (rtc_red_dup_int_hd_symb hyp H2). Funeqtac. auto. Qed.
imports: CoLoR(ADecomp ADuplicateSymb ATrs ListUtil RelSub RelUtil AGraph LogicUtil BoolUtil AShift EqUtil ListDec)