anchor.diff:      choice {
       let! th1 = th1
       let! th2 = th2
  +    // TODO : The next two values should use pattern-matching to return errors when the list
  +    // is empty; as-is, an exception will be raised and the program will crash.
       let tl1 = hyp th1
       let tl2 = hyp th2
       let! tm = mk_disj(hd tl1, hd tl2)
  
positive.code:     let P = parse_term @"P:bool"
      let pth =
          choice {
          // CLEAN : Rename these values to something sensible.
          let! foo1 = ASSUME <| parse_term @"P = F"
          let! foo2 = ASSUME <| parse_term @"P:bool"
          let! th1 = EQ_MP (Choice.result foo1) (Choice.result foo2)
          let! foo3 = EQ_MP F_DEF (Choice.result th1)
          let! foo4 = SPEC (parse_term @"F") (Choice.result foo3)
          let! th2 = DISCH P (Choice.result foo4)
          let! foo5 = NOT_INTRO (Choice.result th2)
  
negative.code:         }
      fun (th : Protected<thm0>) ->
          choice {
          let! pth = pth
          let! th = th
          let tm = concl th
          // CLEAN : Rename these values to something sensible.
          let! foo1 = rator tm
          let! foo2 = rand foo1
          let! foo3 = INST [tm, P] (Choice.result pth)
          return! MP (Choice.result foo3) (Choice.result th)
          }
          |> Choice.mapError (fun e -> nestedFailure e "EQF_ELIM") : Protected<thm0>
  
  