[STATEMENT]
lemma fst_inv_equalityI: 
     assumes surj_h: "surj h"
         and prem:   "!! x y. g (h(x,y)) = x"
     shows "fst (inv h z) = g z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (inv h z) = g z
[PROOF STEP]
by (metis UNIV_I f_inv_into_f prod.collapse prem surj_h)