proposition: Lemma dom_superhereditary : superhereditary dominating.
proof: Proof. apply/superhereditaryP => D F /subsetP DsubF /dominatingP Ddom. apply/dominatingP => v vnotinF. have/Ddom [w winD wv]: v \notin D by apply: contraNN vnotinF; exact: DsubF. exists w => //; exact: DsubF. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)