proposition: Lemma hde_restricted : is_restricted hde D.
proof: Proof. unfold is_restricted. intros. unfold hde in H; tauto. Qed.
imports: CoLoR(ADecomp ADuplicateSymb ATrs ListUtil RelSub RelUtil AGraph LogicUtil BoolUtil AShift EqUtil ListDec)