fact: Definition lift_edge (x y : {i : I & G i}) := (tag x == tag y) && edge (tagged x) (tagged_as x y).
imports: Relations Recdef mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base)