anchor.diff:  /// Applies a function to both sides of an equational theorem.
   let AP_TERM tm th = 
       MK_COMB (REFL tm, th)
  -    |> Choice.mapError (fun _ -> Exception "AP_TERM")
  +    |> Choice.bindError (fun _ -> Choice.failwith "AP_TERM")
   
   /// Proves equality of equal functions applied to a term.
   let AP_THM th tm = 
       MK_COMB (th, REFL tm)
  -    |> Choice.mapError (fun _ -> Exception "AP_THM")
  +    |> Choice.bindError (fun _ -> Choice.failwith "AP_THM")
   
   /// Swaps left-hand and right-hand sides of an equation.
   let SYM th = 
  -    let tm = concl <| Choice.get th
  -    let l, r = Choice.get <| dest_eq tm
  -    let lth = REFL l
  -    EQ_MP (MK_COMB(AP_TERM (Choice.get <| rator(Choice.get <| rator tm)) th, lth)) lth
  -
  -/// Proves equality of Choice.get <| alpha-equivalent terms.
  +    choice {
  +        let! tm = Choice.map concl th
  +        let! l, r = dest_eq tm
  +        let lth = REFL l
  +        let! tm' = rator tm
  +        let! tm'' = rator tm'
  +        return! EQ_MP (MK_COMB(AP_TERM tm'' th, lth)) lth
  +    }
  +
  +/// Proves equality of lpha-equivalent terms.
   let ALPHA tm1 tm2 = 
       TRANS (REFL tm1) (REFL tm2)
  -    |> Choice.mapError (fun _ -> Exception "ALPHA")
  +    |> Choice.bindError (fun _ -> Choice.failwith "ALPHA")
   
   /// Renames the bound variable of a lambda-abstraction.
   let ALPHA_CONV v tm = 
  -    let res = Choice.get <| alpha v tm
  -    ALPHA tm res
  +    alpha v tm
  +    |> Choice.bind (ALPHA tm)
   
   /// Renames the bound variable of an abstraction or binder.
   let GEN_ALPHA_CONV v tm = 
       if is_abs tm then ALPHA_CONV v tm
  -    else 
  -        let b, abs = Choice.get <| dest_comb tm
  -        AP_TERM b (ALPHA_CONV v abs)
  +    else
  +        dest_comb tm
  +        |> Choice.bind (fun (b, abs) ->  
  +            AP_TERM b (ALPHA_CONV v abs))
   
   /// Compose equational theorems with binary operator.
   let MK_BINOP op (lth, rth) = MK_COMB(AP_TERM op lth, rth)
  
positive.code: /// Applies two conversions in sequence.
  let THENC : conv -> conv -> conv = 
      fun conv1 conv2 t -> 
          let th1 = conv1 t
          let th2 = conv2 (Choice.get <| rand(concl <| Choice.get th1))
          TRANS th1 th2
  
  /// Applies the first of two conversions that succeeds.
  let ORELSEC : conv -> conv -> conv = 
  
negative.code: /// Applies two conversions to the two sides of an application.
  let COMB2_CONV : conv -> conv -> conv = 
      fun lconv rconv tm -> 
          dest_comb tm
          |> Choice.bind (fun (l, r) ->
              MK_COMB(lconv l, rconv r))
  
  /// Applies a conversion to the two sides of an application.
  let COMB_CONV = W COMB2_CONV
  
  /// Applies a conversion to the body of an abstraction.
  let ABS_CONV : conv -> conv = 
      fun conv tm -> 
          choice {
              let! v, bod = dest_abs tm
              let th = conv bod
              return! ABS v th
              |> Choice.bindError(fun _ ->
                  choice {
                      let! tv = type_of v
                      let gv = genvar tv
                      let! gbod = vsubst [gv, v] bod
                      let gth = ABS gv (conv gbod)
                      let! gtm = Choice.map concl gth
                      let! l, r = dest_eq gtm
                      let! v' = variant (frees gtm) v
                      let! l' = alpha v' l
                      let! r' = alpha v' r
                      let! tm' = mk_eq(l', r')
                      return! EQ_MP (ALPHA gtm tm') gth
                  })
          }
  
  /// Applies conversion to the body of a binder.
  let BINDER_CONV conv tm = 
      if is_abs tm then ABS_CONV conv tm
      else RAND_CONV (ABS_CONV conv) tm
  