proposition: Lemma lift_eq (i : I) (x y : G i) : lift_edge (existT i x) (existT i y) = edge x y.
proof: Proof. by rewrite /lift_edge /= eqxx tagged_asE. Qed.
imports: Relations Recdef mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base)