assume [A] : (B)

infer (C | D)

  case (C)
  infer (E)
  lookup (E)

  case (D)
  infer (F)
  lookup contradiction
