proposition: Lemma UM_select_correct (u : sform) (x : UMType) : u \in val x -> isDia u -> suppC (val (UM_select u x)) (body u |` R (val x)).
proof: Proof. move => in_x dia_u. rewrite /UM_select. move: (erefl (u \in val x)). rewrite {2 3}in_x => e. destruct u as [[|p|s t|s] [|]] => //. exact: (xchooseP (UMP e (valP x) (erefl _))). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)