proposition: Lemma connect_in1 (x y : T) : x \in S -> y \in S -> e x y -> connect_in x y.
proof: Proof. move => x_inS y_inS xy. apply/existsP; exists (SeqSub _ x_inS). apply/existsP; exists (SeqSub _ y_inS). by rewrite /= !eqxx connect1. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)