anchor.diff:      let p = parse_term @"p:bool"
       let q = parse_term @"q:bool"
       let pth =
  -        let th1 = BETA_RULE(AP_THM (AP_THM IMP_DEF p) q)
  -        let th2 = EQ_MP th1 (ASSUME <| parse_term @"p ==> q")
  -        CONJUNCT2(EQ_MP (SYM th2) (ASSUME <| parse_term @"p:bool"))
  +        choice {
  +        let! IMP_DEF = IMP_DEF
  +        let! foo1 = AP_THM (Choice.result IMP_DEF) p
  +        let! foo2 = AP_THM (Choice.result foo1) q
  +        let! th1 = BETA_RULE (Choice.result foo2)
  +        let! foo3 = ASSUME <| parse_term @"p ==> q"
  +        let! th2 = EQ_MP (Choice.result th1) (Choice.result foo3)
  +        let! foo4 = SYM (Choice.result th2)
  +        let! foo5 = ASSUME <| parse_term @"p:bool"
  +        let! foo6 = EQ_MP (Choice.result foo4) (Choice.result foo5)
  +        return! CONJUNCT2 (Choice.result foo6)
  +        }
       fun (ith : Protected<thm0>) (th : Protected<thm0>) -> 
           choice {
  -            let! tm = Choice.map concl ith
  -            let! ant, con = dest_imp tm
  -            let! tm' = Choice.map concl th
  -            if aconv ant tm' then 
  -                return! PROVE_HYP th (PROVE_HYP ith (INST [ant, p; con, q] pth))
  -            else 
  -                return! Choice.failwith "MP: theorems do not agree"
  +        let! pth = pth
  +        let! ith = ith
  +        let! th = th
  +        let tm = concl ith
  +        let! ant, con = dest_imp tm
  +        let tm' = concl th
  +        if aconv ant tm' then
  +            let! foo1 = INST [ant, p; con, q] (Choice.result pth)
  +            let! foo2 = PROVE_HYP (Choice.result ith) (Choice.result foo1)
  +            return! PROVE_HYP (Choice.result th) (Choice.result foo2)
  +        else 
  +            return! Choice.failwith "MP: theorems do not agree"
           } : Protected<thm0>
   
   /// Discharges an assumption.
  
positive.code:     }
  
  /// Deduces equality of boolean terms from forward and backward implications.
  let IMP_ANTISYM_RULE (th1 : Protected<thm0>) (th2 : Protected<thm0>) =
      choice {
      let! th1 = th1
      let! th2 = th2
  
negative.code: let CONJUNCT2 = 
      let P = parse_term @"P:bool"
      let Q = parse_term @"Q:bool"
      let pth =
          choice {
          let! AND_DEF = AND_DEF
          let! foo1 = AP_THM (Choice.result AND_DEF) <| parse_term @"P:bool"
          let! th1 = CONV_RULE (RAND_CONV BETA_CONV) (Choice.result foo1)
          let! foo2 = AP_THM (Choice.result th1) <| parse_term @"Q:bool"
          let! th2 = CONV_RULE (RAND_CONV BETA_CONV) (Choice.result foo2)
          let! foo3 = ASSUME <| parse_term @"P /\ Q"
          let! th3 = EQ_MP (Choice.result th2) (Choice.result foo3)
          let! foo4 = AP_THM (Choice.result th3) <| parse_term @"\(p:bool) (q:bool). q"
          let! foo5 = BETA_RULE (Choice.result foo4)
          return! EQT_ELIM (Choice.result foo5)
          }
      fun (th : Protected<thm0>) ->
          choice {
          let! pth = pth
          let! th = th
          let tm = concl th
          let! l, r = dest_conj tm
          let! foo1 = INST [l, P; r, Q] (Choice.result pth)
          return! PROVE_HYP (Choice.result th) (Choice.result foo1)
          }
          |> Choice.mapError (fun e -> nestedFailure e "CONJUNCT2") : Protected<thm0>
  
  