proposition: Lemma connect_subtype (T : finType) (x0 : T) (e : rel T) (Tp : subFinType (connect e x0)) : forall x p, connect (restrict Tp e) (Sub x0 p) x.
proof: Proof. move => x. case: (SubP x) => {x} - x Px. case/connectP : Px (Px) => pth. elim/last_ind: pth x => [x _ -> Px /= p|pth y IH x /=]. - by rewrite (bool_irrelevance p Px) connect0. - rewrite rcons_path last_rcons. case/andP => Pth xy E Px p. subst. have conn : connect e x0 (last x0 pth) by apply/connectP; exists pth. apply: connect_trans. + exact: IH. + apply: connect1. by rewrite /restrict !SubK. Qed.
imports: Relations Recdef mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base)