[STATEMENT]
lemma "(\<lambda>f x y. (curry o case_prod) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. curry \<circ> case_prod = (\<lambda>f. f)
[PROOF STEP]
nitpick [card = 1-12, expect = none]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. curry \<circ> case_prod = (\<lambda>f. f)
[PROOF STEP]
by auto