anchor.diff:          fun tac1 tac2l g -> 
               tac1 g
               |> Choice.map (fun (_, gls, _ as gstate) ->
  -                if gls = []
  -                then tacsequence gstate []
  +                if gls = [] then 
  +                    tacsequence gstate []
                   else tacsequence gstate tac2l)
       then_, thenl_
   
  
positive.code: 
  /// Sequentially applies all the tactics in a given list of tactics.
  let EVERY tacl =
      itlist (fun t1 t2 -> t1 |> THEN <| t2) tacl ALL_TAC
  
  /// Applies the first tactic in a tactic list that succeeds.
  let FIRST : tactic list -> tactic =
      fun tacl g -> end_itlist (fun t1 t2 -> t1 |> ORELSE <| t2) tacl g;;
  
  /// Sequentially applies all tactics given by mapping a function over a list.
  let MAP_EVERY (tacf : 'T -> tactic) (lst : 'T list) : tactic = 
  
negative.code: /// Solves a goal that is an equation between alpha-equivalent terms.
  let (REFL_TAC : tactic) = 
      fun ((asl, w) as g) -> 
          choice {
              let! tm = rand w
              return! ACCEPT_TAC (REFL tm) g
          }
          |> Choice.mapError (fun e -> nestedFailure e "REFL_TAC")
  
  /// Strips an abstraction from each side of an equational goal.
  