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 LET_DEF = new_definition(parse_term @"LET (f:A->B) x = f x")
  
  let LET_END_DEF = new_definition(parse_term @"LET_END (t:A) = t")
  
  let GABS_DEF = new_definition(parse_term @"GABS (P:A->bool) = (@) P")
  
  let GEQ_DEF = new_definition(parse_term @"GEQ a b = (a:A = b)")
  
  let _SEQPATTERN = 
      new_definition
          (parse_term @"_SEQPATTERN = \r s x. if ?y. r x y then r x else s x")
  
  let _UNGUARDED_PATTERN = 
      new_definition(parse_term @"_UNGUARDED_PATTERN = \p r. p /\ r")
  
  let _GUARDED_PATTERN = 
      new_definition(parse_term @"_GUARDED_PATTERN = \p g r. p /\ g /\ r")
  
  let _MATCH = 
      new_definition
          (parse_term @"_MATCH =  \e r. if (?!) (r e) then (@) (r e) else @z. F")
  
  let _FUNCTION = 
      new_definition
          (parse_term @"_FUNCTION = \r x. if (?!) (r x) then (@) (r x) else @z. F")
  