[STATEMENT]
lemma "fst (x, y::'a\<Rightarrow>'b) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (x, y) = x
[PROOF STEP]
nitpick [expect = none]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (x, y) = x
[PROOF STEP]
by (simp add: fst_def)