proposition: Lemma liftE (i j : I) (x : G i) (y : G j) : lift_edge (existT i x) (existT j y) -> j = i.
proof: Proof. by case/andP => /= /eqP. Qed.
imports: Relations Recdef mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base)