proposition: Lemma hde_dec : forall r1 r2, {hde r1 r2} + {~hde r1 r2}.
proof: Proof. intros. unfold hde. destruct (In_dec eq_rule_dec r1 D); try tauto. destruct (In_dec eq_rule_dec r2 D); try tauto. destruct (rhs r1). left; auto. destruct (lhs r2); auto. destruct (eq_symb_dec f f0); try tauto. Defined.
imports: CoLoR(ADecomp ADuplicateSymb ATrs ListUtil RelSub RelUtil AGraph LogicUtil BoolUtil AShift EqUtil ListDec)