assume [A] : (B)
goal P

infer (C | D | G)

  case (C)
  infer (E)
  lookup goal

  case (D)
  infer (F)
  lookup contradiction

  case (G)
  infer (H)
  lookup goal
