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:     else 
          fun (asl, w) ->
              choice {
                  let! x, bod =
                      dest_forall w
                      |> Choice.mapError (fun e -> nestedFailure e "X_GEN_TAC: Not universally quantified")
  
                  do! tactic_type_compatibility_check "X_GEN_TAC" x x'
                  let! asl' = Choice.List.map snd asl
                  let avoids = itlist (union << thm_frees) asl' (frees w)
                  if mem x' avoids then
                      return! Choice.failwith "X_GEN_TAC: invalid variable"
                  else 
                      let afn = CONV_RULE (GEN_ALPHA_CONV x)
                      let fun1 l =
                          match l with
                          | [a] -> a
                          | _ -> Choice.failwith "X_GEN_TAC.fun1: Unhandled case."
                      let! tm = vsubst [x', x] bod
                      return (null_meta, [asl, tm], fun i tl -> afn (GEN x' (fun1 tl)))
              }
  
  /// Assumes a theorem, with existentially quantified variable replaced by a given witness.
  let X_CHOOSE_TAC x' (xth : thm) : tactic =
      let xtm = Choice.map concl xth
      let xbod = Choice.bind dest_exists xtm
      do
          xbod |> Choice.iter (fun (x, _) ->
              tactic_type_compatibility_check "X_CHOOSE_TAC" x x' |> ignore)
  
      let pat = xbod |> Choice.bind (fun (x, bod) -> vsubst [x', x] bod)
      let xth' = Choice.bind ASSUME pat
      fun (asl, w) -> 
          choice {
              let! xtm = xtm
              let! x, bod = xbod |> Choice.mapError (fun e -> nestedFailure e "X_CHOOSE_TAC: not existential") 
              let! pat = pat
              let xth' = xth'
  
              let! asl' = Choice.List.map snd asl
              let! tms = Choice.map thm_frees xth
              let avoids = 
                  itlist (union << frees << concl) asl' (union (frees w) tms)
              if mem x' avoids then
                  return! Choice.failwith "X_CHOOSE_TAC: invalid variable"
              else 
                  let fun1 l =
                      match l with
                      | [a] -> a
                      | _ -> Choice.failwith "X_CHOOSE_TAC.fun1: Unhandled case."
                  return (null_meta, [("", xth') :: asl, w], fun i tl -> CHOOSE (x', INSTANTIATE_ALL i xth) (fun1 tl))                
          }
  
  /// Reduces existentially quantified goal to one involving a specific witness.
  let EXISTS_TAC t : tactic =
      fun (asl, w) ->
          choice {
              let! v, bod = 
                  dest_exists w
                  |> Choice.mapError (fun e -> nestedFailure e "EXISTS_TAC: Goal not existentially quantified")
              do! tactic_type_compatibility_check "EXISTS_TAC" v t
              let fun1 l =
                  match l with
                  | [a] -> a
                  | _ -> Choice.failwith "EXISTS_TAC.fun1: Unhandled case."
              let! tm = vsubst [t, v] bod
              return (null_meta, [asl, tm], fun i tl -> EXISTS (Choice.get <| instantiate i w, Choice.get <| instantiate i t) (fun1 tl))
          }
  
  /// Strips the outermost universal quantifier from the conclusion of a goal.
  let (GEN_TAC : tactic) = 
      fun (asl, w) -> 
          choice { 
              let! (x, _) = dest_forall w
              let! asl' = Choice.List.map snd asl
              let avoids = itlist (union << thm_frees) asl' (frees w)
              let! x' = mk_primed_var avoids x
              return! X_GEN_TAC x' (asl, w)
          }
          |> Choice.mapError (fun e -> nestedFailure e "GEN_TAC")
  
  /// Adds the body of an existentially quantified theorem to the assumptions of a goal.
  let (CHOOSE_TAC : thm_tactic) = 
  