anchor.diff:      prove
           ((parse_term @"!x:A#B. FST x,SND x = x"), 
            GEN_TAC
  -         |> THEN <| (X_CHOOSE_THEN (parse_term @"a:A") 
  +         |> THEN 
  +         <| (X_CHOOSE_THEN (parse_term @"a:A") 
                    (X_CHOOSE_THEN (parse_term @"b:B") SUBST1_TAC) 
                    (SPEC (parse_term @"x:A#B") PAIR_SURJECTIVE))
            |> THEN <| REWRITE_TAC [FST; SND])
  
positive.code: 
  let PAIR_EXISTS_THM = 
      prove((parse_term @"?x. ?(a:A) (b:B). x = mk_pair a b"), MESON_TAC [])
  let prod_tybij = 
      new_type_definition "prod" ("ABS_prod", "REP_prod") PAIR_EXISTS_THM
  let REP_ABS_PAIR = 
      prove
          ((parse_term 
  
negative.code: 
  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)")
  