proposition: Lemma uncurry_curry : forall A B C, @uncurry A B C ∘ curry = id.
proof: Proof. simpl ; intros. unfold curry, uncurry, compose. extensionality x ; extensionality p. destruct p ; simpl ; reflexivity. Qed.
imports: Coq.Program.Basics FunctionalExtensionality