proposition: Lemma UM_trans_R (x y : UM) : trans x y -> suppC (val y) (R (val x)).
proof: Proof. case/hasP => u u1 /andP [u2 /eqP ->]. move: (UM_select_correct u1 u2). rewrite suppCU. by bcase. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)