anchor.diff:  
   let UNCURRY_DEF = 
       new_definition(parse_term @"!f x y. UNCURRY(f:A->B->C)(x,y) = f x y")
  +
   let PASSOC_DEF = 
       new_definition
           (parse_term @"!f x y z. PASSOC (f:(A#B)#C->D) (x,y,z) = f ((x,y),z)")
  
positive.code:          REPEAT GEN_TAC
           |> THEN <| EQ_TAC
           |> THENL <| [REWRITE_TAC [COMMA_DEF]
                        |> THEN <| DISCH_THEN (MP_TAC << AP_TERM(parse_term @"REP_prod:A#B->A->B->bool"))
                        |> THEN <| REWRITE_TAC [REP_ABS_PAIR]
                        |> THEN <| REWRITE_TAC [mk_pair_def; FUN_EQ_THM]
                        ALL_TAC]
           |> THEN <| MESON_TAC [])
  
  let PAIR_SURJECTIVE = 
      prove(
          (parse_term @"!p:A#B. ?x y. p = x,y"),
          GEN_TAC
          |> THEN <| REWRITE_TAC [COMMA_DEF]
          |> THEN <| MP_TAC (SPEC (parse_term "REP_prod p :A->B->bool") (CONJUNCT2 prod_tybij))
          |> THEN <| REWRITE_TAC [CONJUNCT1 prod_tybij]
          |> THEN <| DISCH_THEN
                  (X_CHOOSE_THEN
                      (parse_term @"a:A") 
                      (X_CHOOSE_THEN (parse_term "b:B") MP_TAC))
          |> THEN <| DISCH_THEN
                  (MP_TAC << AP_TERM (parse_term "ABS_prod:(A->B->bool)->A#B"))
          |> THEN <| REWRITE_TAC 
                  [CONJUNCT1 prod_tybij]
          |> THEN <| DISCH_THEN SUBST1_TAC
          |> THEN <| MAP_EVERY EXISTS_TAC 
                  [(parse_term @"a:A")
                   (parse_term @"b:B")]
          |> THEN <| REFL_TAC)
  
  let FST = 
      prove
  
negative.code:         let rec depair gv arg = 
              try 
                  let l, r = dest_pair arg
                  (depair (list_mk_icomb "FST" [gv]) l) @ (depair (list_mk_icomb "SND" [gv]) r) //deleted new line before @
              with
              | Failure _ -> [gv, arg]
          fun arg -> 
  