proposition: Theorem uncurry_curry : forall (X Y Z : Type) (f : X -> Y -> Z) x y, prod_curry (prod_uncurry f) x y = f x y.
proof: Proof. Admitted. Theorem curry_uncurry : forall (X Y Z : Type) (f : (X * Y) -> Z) (p : X * Y), prod_uncurry (prod_curry f) p = f p. Proof. Admitted. Definition manual_grade_for_informal_proof : option (nat*string) := None. Module Church. Definition cnat := forall X : Type, (X -> X) -> X -> X. Definition one : cnat := fun (X : Type) (f : X -> X) (x : X) => f x. Definition two : cnat := fun (X : Type) (f : X -> X) (x : X) => f (f x). Definition zero : cnat := fun (X : Type) (f : X -> X) (x : X) => x. Definition three : cnat := @doit3times. Definition zero' : cnat := fun (X : Type) (succ : X -> X) (zero : X) => zero. Definition one' : cnat := fun (X : Type) (succ : X -> X) (zero : X) => succ zero. Definition two' : cnat := fun (X : Type) (succ : X -> X) (zero : X) => succ (succ zero). Example zero_church_peano : zero nat S O = 0. Proof. reflexivity. Qed.