`{Funext} {σ} (A : Carriers σ) {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ) : operation_curry A ss t o operation_uncurry A ss t == idmap. Proof. intro a. induction n; [reflexivity|]. funext x. refine (_ @ IHn (fstail ss) (a x)). refine (ap (operation_curry A (fstail ss) t) _). funext a'. simpl. unfold cons_dom, cons_dom'. rewrite fin_ind_beta_zero. refine (ap (operation_uncurry A (fstail ss) t (a x)) _). funext i'. by rewrite fin_ind_beta_fsucc. Qed.
Require Import