proposition: Lemma set_sub_clns : D1 \subset NS[D1].
proof: Proof. apply/subsetP => x xinD1. apply/bigcupP; exists x => //. exact: v_in_clneigh. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)