proposition: Lemma UM_trans_D (x : UM) s : fAX s^- \in val x -> exists2 y : UM, trans x y & val y |> s^-.
proof: Proof. move => H. exists (UM_select (fAX s^-) x). - apply/hasP. by exists (fAX s^-) => //=. - move: (UM_select_correct H (erefl _)). by rewrite suppCU suppC1 /=; bcase. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)