proposition: Lemma sub_induced (A : {set induced}) : val @: A \subset S.
proof: Proof. by apply/subsetP => ? /imsetP[x xH ->]; apply: valP. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)