anchor.diff:  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."
  -        return (null_meta, [asl, Choice.get <| mk_forall(x, Choice.get <| subst [x, t] w)], fun i tl -> SPEC (Choice.get <| instantiate i t) (fun1 tl))
  +            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.")
   
  
positive.code:     else 
          fun (asl, w) ->
              choice {
              let! x, bod =
                  try
                      dest_forall w
                  with
                  | Failure _ as e ->
                      Choice.nestedFailwith e "X_GEN_TAC: Not universally quantified"
              do! tactic_type_compatibility_check "X_GEN_TAC" x x'
              let avoids = itlist (union << thm_frees << Choice.get << snd) 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."
                  return (null_meta, [asl, Choice.get <| vsubst [x', x] bod], 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 = concl <| Choice.get xth
      let x, bod = 
          try 
              Choice.get <| dest_exists xtm
          with
          | Failure _ as e ->
              nestedFailwith e "X_CHOOSE_TAC: not existential"
      do
          tactic_type_compatibility_check "X_CHOOSE_TAC" x x'
          |> Choice.get
      let pat = Choice.get <| vsubst [x', x] bod
      let xth' = ASSUME pat
      fun (asl, w) -> 
          let avoids = 
              itlist (union << frees << concl << Choice.get << snd) asl 
                  (union (frees w) (thm_frees <| Choice.get xth))
          if mem x' avoids then
              Choice.failwith "X_CHOOSE_TAC: invalid variable"
          else 
              let fun1 l =
                  match l with
                  | [a] -> a
                  | _ -> Choice.failwith "X_CHOOSE_TAC.fun1: Unhandled case."
              (null_meta, [("", xth') :: asl, w], fun i tl -> CHOOSE (x', INSTANTIATE_ALL i xth) (fun1 tl))
              |> Choice.result
  
  /// Reduces existentially quantified goal to one involving a specific witness.
  let EXISTS_TAC t : tactic =
      fun (asl, w) ->
          choice {
          let! v, bod = 
              try 
                  dest_exists w
              with
              | Failure _ as e ->
                  Choice.nestedFailwith 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."
          return (null_meta, [asl, Choice.get <| vsubst [t, v] bod], 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) -> 
          try 
              let x = fst(Choice.get <| dest_forall w)
              let avoids = itlist (union << thm_frees << Choice.get << snd) asl (frees w)
              let x' = Choice.get <| mk_primed_var avoids x
              X_GEN_TAC x' (asl, w)
          with
          | Failure _ as e ->
              Choice.nestedFailwith e "GEN_TAC"
  
  /// Adds the body of an existentially quantified theorem to the assumptions of a goal.
  let (CHOOSE_TAC : thm_tactic) = 
  
negative.code: /// Strips an abstraction from each side of an equational goal.
  let (ABS_TAC : tactic) = 
      fun (asl, w) -> 
          choice { 
              let! l, r = dest_eq w
              let! lv, lb = dest_abs l
              let! rv, rb = dest_abs r
              let! asl' = Choice.List.map snd asl
              let avoids = itlist (union << thm_frees) asl' (frees w)
              let! v = mk_primed_var avoids lv
              let! tm1 = vsubst [v, lv] lb
              let! tm2 = vsubst [v, rv] rb
              let! tm3 = mk_eq(tm1, tm2)
              return 
                  (null_meta, [asl, tm3], 
                   fun i tl -> 
                      let fun1 l =
                          match l with
                          | [a] -> a
                          | _ -> Choice.failwith "ABS_TAC.fun1: Unhandled case."
                      choice {
                          let ath = ABS v (fun1 tl)
                          let! tm = Choice.map concl ath
                          return! EQ_MP (ALPHA tm (Choice.get <| instantiate i w)) ath
                      })            
          }
          |> 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) -> 
          choice { 
              let fun1 l =
                  match l with
                  | [a1; a2] -> (a1, a2)
                  | _ -> failwith "MK_COMB_TAC.fun1: Unhandled case."
              let! l, r = dest_eq gl
              let! f, x = dest_comb l
              let! g, y = dest_comb r
              let! tm1 = mk_eq(f, g)
              let! tm2 = mk_eq(x, y)
              return (null_meta, [asl, tm1; asl, tm2], fun _ tl -> MK_COMB (fun1 tl))            
          } 
          |> 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) =
  