(llvmctx : LLVM.Context) →
  (motive : Except Lean.IR.EmitLLVM.Error (Unit × Lean.IR.EmitLLVM.State llvmctx) → Sort u_1) →
    (out? : Except Lean.IR.EmitLLVM.Error (Unit × Lean.IR.EmitLLVM.State llvmctx)) →
      ((a : Unit × Lean.IR.EmitLLVM.State llvmctx) → motive (Except.ok a)) →
        ((err : Lean.IR.EmitLLVM.Error) → motive (Except.error err)) → motive out?