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[]; ] );;