proposition: Proposition superhereditaryP (p : pred {set T}) : reflect (forall D F : {set T}, (D \subset F) -> p D -> p F) (superhereditary p).
proof: Proof. apply: (iffP (hereditaryP _)) => /= sh_p D F. all: by rewrite -setCS => /sh_p; rewrite ?setCK; auto. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)