proposition: Proposition minimal_indsysP p D : superhereditary p -> reflect (p D /\ forall v : T, v \in D -> ~~ p (D :\ v)) (minset p D).
proof: Proof. rewrite minmaxset => sh_p; apply: (iffP (maximal_indsysP _ _)) => //=. all: rewrite ?setCK => -[pD H]; split => // v; move: (H v). all: by rewrite !inE ?setCU ?setCK ?negbK setDE setIC. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)