proposition: Lemma subset_dfs n v a : v \subset foldl (dfs n) v a.
proof: Proof. elim: n a v => [|n IHn]; first by elim=> //= *; rewrite if_same. elim=> //= x a IHa v; apply: subset_trans {IHa}(IHa _); case: ifP => // _. by apply: subset_trans (IHn _ _); apply/subsetP=> y; apply: predU1r. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)