fact: Definition UM_trans (x y : UMType) := [some u in val x, isDia u && (y == UM_select u x)].
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)