proposition: Lemma connect_in_trans (z x y : T) : connect_in x z -> connect_in z y -> connect_in x y.
proof: Proof. rewrite /connect_in. move => /existsP [a] /existsP [b] /and3P [/eqP ? /eqP ? ?] /existsP [?] /existsP [c] /and3P [/eqP H /eqP ? R]. subst. apply/existsP; exists a. apply/existsP; exists c. rewrite !eqxx /=. apply: connect_trans _ R. by rewrite (val_inj H). Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)