anchor.diff:  
   /// Use an equation to substitute "safely" in goal.
   let SUBST_VAR_TAC (th : thm) g : goalstate = 
  -    let v = 
  -        let asm, eq = dest_thm <| Choice.get th
  -        let l, r = Choice.get <| dest_eq eq
  -        if aconv l r
  -        then ALL_TAC g
  -        elif not(subset (frees eq) (freesl asm))
  -        then Choice.failwith ""
  -        elif (is_const l || is_var l) && not(free_in l r)
  -        then SUBST_ALL_TAC th g
  -        elif (is_const r || is_var r) && not(free_in r l)
  -        then SUBST_ALL_TAC (SYM th) g
  -        else Choice.failwith ""
  -    v |> Choice.mapError (fun e -> nestedFailure e "SUBST_VAR_TAC")
  +    choice { 
  +        let! asm, eq = Choice.map dest_thm th
  +        let! l, r = dest_eq eq
  +        if aconv l r then 
  +            return! ALL_TAC g
  +        elif not(subset (frees eq) (freesl asm)) then 
  +            return! Choice.failwith ""
  +        elif (is_const l || is_var l) && not(free_in l r) then 
  +            return! SUBST_ALL_TAC th g
  +        elif (is_const r || is_var r) && not(free_in r l) then
  +            return! SUBST_ALL_TAC (SYM th) g
  +        else 
  +            return! Choice.failwith ""
  +    } 
  +    |> Choice.mapError (fun e -> nestedFailure e "SUBST_VAR_TAC")
   
   (* ------------------------------------------------------------------------- *)
   (* Basic logical tactics.                                                    *)
  
positive.code: /// Strips an abstraction from each side of an equational goal.
  let (ABS_TAC : tactic) = 
      fun (asl, w) -> 
          let v = 
              let l, r = Choice.get <| dest_eq w
              let lv, lb = Choice.get <| dest_abs l
              let rv, rb = Choice.get <| dest_abs r
              let avoids = itlist (union << thm_frees << Choice.get << snd) asl (frees w)
              let v = Choice.get <| mk_primed_var avoids lv
              (null_meta, [asl, Choice.get <| mk_eq(Choice.get <| vsubst [v, lv] lb, Choice.get <| vsubst [v, rv] rb)], 
               fun i tl -> 
                  let fun1 l =
                      match l with
                      | [a] -> a
                      | _ -> Choice.failwith "ABS_TAC.fun1: Unhandled case."
                  let ath = ABS v (fun1 tl)
                  EQ_MP (ALPHA (concl <| Choice.get ath) (Choice.get <| instantiate i w)) ath)
              |> Choice.result
          v |> Choice.mapError (fun e -> nestedFailure e "ABS_TAC: Failure.")
  
  /// Breaks down a goal between function applications into equality of functions and arguments.
  let (MK_COMB_TAC : tactic) = 
      fun (asl, gl) -> 
          let v = 
              let fun1 l =
                  match l with
                  | [a1; a2] -> (a1, a2)
                  | _ -> failwith "MK_COMB_TAC.fun1: Unhandled case."
              let l, r = Choice.get <| dest_eq gl
              let f, x = Choice.get <| dest_comb l
              let g, y = Choice.get <| dest_comb r
              (null_meta, [asl, Choice.get <| mk_eq(f, g); asl, Choice.get <| mk_eq(x, y)], fun _ tl -> MK_COMB (fun1 tl))
              |> Choice.result
          v |> Choice.mapError (fun e -> nestedFailure e "MK_COMB_TAC: Failure.")
  
  /// Strips a function application from both sides of an equational goal.
  let (AP_TERM_TAC : tactic) =
  
negative.code: let (SPEC_TAC : term * term -> tactic) = 
      fun (t, x) (asl, w) ->
          choice {
              let fun1 l =
                  match l with
                  | [a] -> a
                  | _ -> Choice.failwith "LABEL_TAC.fun1: Unhandled case."
              let! tm1 = subst [x, t] w
              let! tm2 = mk_forall(x, tm1)
              return (null_meta, [asl, tm2], fun i tl -> SPEC (Choice.get <| instantiate i t) (fun1 tl))
          }
          |> Choice.mapError (fun e -> nestedFailure e "SPEC_TAC: Failure.")
  
  