proposition: Lemma connect_inP x y : reflect (exists p : seq T, [/\ all (mem S) (x::p), path e x p & y = last x p]) (connect_in x y).
proof: Proof. apply: (iffP idP). - case/existsP => a. case/existsP => b. case/and3P => [/eqP ? /eqP ?]. subst. case/connectP => p P1 P2. exists (map val p). rewrite /= ssvalP /=. elim: p a P1 P2 => //= [? _ -> //| c p IHp a]. case/andP => [He ?] ?. rewrite ssvalP He //=. exact: IHp. - case => p. elim: p x => /=. + move => x [/andP [inS _] ? ->]. exact: connect_in0. + move => z p IHp x [/and3P [x_inS y_inS ?] /andP [? ?] ?]. apply: (@connect_in_trans z); first exact: connect_in1. by apply: IHp; rewrite y_inS. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)