let pre_beta = prove_by_refinement
(`!g u' v'. (?f. (!u v. f { u, v } = (g:A->A->B) u v)) ==> 
    ((\ { u, v}. g u v) {u',v'} = g u' v')`,
[
REWRITE_TAC[GABS_DEF;GEQ_DEF];
SELECT_ELIM_TAC;
MESON_TAC[];
]);;

let WELLDEFINED_FUNCTION_2 = prove_by_refinement(
`(?f:C->D. (!x:A y:B.  f(s x y) = t x y)) <=> 
   (!x x' y y'.  (s x y = s x' y') ==> t x y = t x' y')`,
[
  MATCH_MP_TAC EQ_TRANS ;
  EXISTS_TAC  `?f:C->D. !z. !x:A y:B. (s x y = z) ==> f z = t x y`;
  CONJ_TAC;
  MESON_TAC[];
  REWRITE_TAC[GSYM SKOLEM_THM];
  MESON_TAC[];
]);;

let well_defined_unordered_pair = prove_by_refinement
(`(?f. (!u v. f { u, v} = (g:A->A->B) u v)) <=>
   (! u v. g u v = g v u)`,
[
REWRITE_TAC[WELLDEFINED_FUNCTION_2];
SUBGOAL_THEN `!u v x' y'. ({u,v} = {x',y'}) <=> ((((u:A)=x') /\ (v = y'))\/ ((u= y') /\ (v = x')))` ASSUME_TAC;
SET_TAC[];
ASM_REWRITE_TAC[];
MESON_TAC[];
]
);;

let BETA_PAIR_THM = prove_by_refinement(
`!g u' v'. (!u v. (g:A->A->B) u v = g v u) ==> 
    ((\ { u, v}. g u v) {u',v'} = g u' v')`,
[
REPEAT STRIP_TAC;
MATCH_MP_TAC pre_beta;
REWRITE_TAC[well_defined_unordered_pair];
ASM_REWRITE_TAC[];
]
);;