{σ} (A : Carriers σ) {n : nat} : forall (ss : FinSeq n (Sort σ)) (t : Sort σ), FiniteOperation A ss t -> CurriedOperation A ss t := match n with | 0 => fun ss t op => op (Empty_ind _) | n'.+1 => fun ss t op x => A (fstail ss) t (op o cons_dom A ss x) end. Local Example computation_example_operation_curry : forall (σ : Signature) (A : Carriers σ) (n : nat) (s1 s2 t : Sort σ) (ss := (fscons s1 (fscons s2 fsnil))) (op : FiniteOperation A ss t) (x1 : A s1) (x2 : A s2), A ss t op = fun x1 x2 => op (cons_dom A ss x1 (cons_dom A _ x2 (nil_dom A _))). Proof. reflexivity. Qed.
Require Import