proposition: Lemma restricted_dp_graph : is_restricted dp_graph DP.
proof: Proof. unfold is_restricted, dp_graph, inclusion. intros. intuition. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)