proposition: Proposition hereditaryP p : reflect (forall D F : {set T}, (F \subset D) -> p D -> p F) (hereditary p).
proof: Proof. apply: (iffP forall_inP) => [H1 D F FsubD pD|H2 D pD]. - exact: (forall_inP (H1 _ pD)). - apply/forall_inP => F FsubD; exact: H2 pD. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)