proposition: Lemma uncurry4_curry4 {A B C D E} (f : A * B * C * D → E) p : uncurry4 (curry4 f) p = f p.
proof: Proof. destruct p as [[[??] ?] ?]; reflexivity. Qed.
imports: Coq(Permutation) Coq.ssr((notations) ssrfun) stdpp(options)