∀ {ps : Std.Do.PostShape} {α : Type u_1} (x : OptionT (Std.Do.PredTrans ps) α),
  Std.Do.PredTrans.Conjunctive fun Q =>
    x.apply
      (fun x =>
        match x with
        | some a => Q.1 a
        | none => Q.2.1 PUnit.unit,
        Q.2.2)