proposition: Lemma irr_hereditary : hereditary irredundant.
proof: Proof. apply/hereditaryP. move=> D F FsubD /irredundantP Dirr. apply/irredundantP => v vinF. move: (subsetP FsubD v vinF) => vinD. move: (Dirr v vinD). case/set0Pn => x /privateP [vdomx H1]. apply/set0Pn; exists x. apply/privateP ; split=> //. move=> u uinF udomx. move: (subsetP FsubD u uinF) => uinD. exact: (H1 u uinD udomx). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)