assume [P] : (G)
goal M

infer (A | B)

  case (A)

  infer (A1 | A2)

  case (A1)
  infer (X1)
  infer (X2)
  lookup goal

  case (A2)
  infer (Y1)
  infer (Y2)
  lookup goal

  case (B)
  infer (F)
  lookup contradiction

