`{Funext} {σ} (A : Carriers σ) {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ) : operation_uncurry A ss t o operation_curry A ss t == idmap. Proof. intro a. induction n as [| n IHn]. - funext d. refine (ap a _). apply path_contr. - funext a'. refine (ap (fun x => x _) (IHn _ _) @ _). refine (ap a _). apply expand_cons_dom. Qed.
Require Import