{ctx : LLVM.Context} →
  (motive : Option (LLVM.Value ctx) → Sort u_1) →
    (__do_lift : Option (LLVM.Value ctx)) →
      ((fn : LLVM.Value ctx) → motive (some fn)) → (Unit → motive none) → motive __do_lift