fact: Definition UM_select (u : sform) (x:UMType) : UMType := (if u \in val x as b return u \in val x = b -> UMType then fun b => (if u is fAX s^- as c return u = c -> UMType then fun e => (xchoose (UMP b (valP x) e)) else fun _ => UM_default) erefl else fun _ => UM_default) erefl.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)