proposition: Lemma connect_in0 (x : T) : x \in S -> connect_in x x.
proof: Proof. move => inS. do 2 (apply/existsP; exists (SeqSub x inS)). by rewrite /= eqxx connect0. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)