proposition: Lemma lift_connect (i : I) (x y : G i) : connect (@edge _ (G i)) x y -> connect lift_edge (existT i x) (existT i y).
proof: Proof. case/connectP => p. elim: p x y => /= [x y _ ->|z p IHp x y /andP [? ?] ?]; first exact: connect0. apply: (@connect_trans _ _ (existT i z)); last exact: IHp. by rewrite connect1 // lift_eq. Qed.
imports: Relations Recdef mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base)