proposition: Lemma UM_trans_bound x y : UM_trans x y -> y \in UM_bound x.
proof: Proof. case/hasP => s s1 /andP[s2 s3]. apply/fimsetP. exists s; last exact/eqP. by rewrite inE s1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)