anchor.diff:      }
   
   /// Deduces equality of boolean terms from forward and backward implications.
  -let IMP_ANTISYM_RULE (th1 : Protected<thm0>) (th2 : Protected<thm0>) =
  +let IMP_ANTISYM_RULE (th1 : Protected<thm0>) (th2 : Protected<thm0>) : Protected<thm0> =
       choice {
       let! th1 = th1
       let! th2 = th2
  
positive.code:     let p = parse_term @"p:bool"
      let q = parse_term @"q:bool"
      let pth =
          
          SYM(BETA_RULE(AP_THM (AP_THM IMP_DEF p) q))
      fun a th -> 
          choice {
              let th1 = CONJ (ASSUME a) th
              let! tm1 = Choice.map concl th1
              let th2 = CONJUNCT1(ASSUME tm1)
              let th3 = DEDUCT_ANTISYM_RULE th1 th2
              let! tm = Choice.map concl th
              let th4 = INST [a, p; tm, q] pth
              return! EQ_MP th4 th3
          } : Protected<thm0>
  
  /// Discharges all hypotheses of a theorem.
  let rec DISCH_ALL (th : Protected<thm0>) : Protected<thm0> = 
      choice {
          let! th' = th
          match hyp th' with
          | t :: _ ->
              return! DISCH_ALL(DISCH t th) |> Choice.bindError (function Failure _ -> th | e -> Choice.error e) 
          | _ -> 
              return! th
      }
  
  /// Undischarges the antecedent of an implicative theorem.
  
negative.code:     }
  
  /// Adds an assumption to a theorem.
  let ADD_ASSUM tm (th : Protected<thm0>) : Protected<thm0> =
      choice {
      let! th = th
      let! foo1 = DISCH tm (Choice.result th)
  