fact: Definition p_until (p q : X -> Prop) pi := exists2 n, forall m, m < n -> p (pi m) & q (pi n).
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)