fact: Fixpoint curry {σ} {V} {o} (a: Applied σ o): Term σ V (ne_list.one o) := match a in (Applied _ s) with | AppliedOp _ op y => apply_args y (app_tree σ (Op σ V op)) | AppliedVar _ v x => Var σ V v x end with apply_args {σ} {V} {o} (a: @Arguments σ V o): op_type (Term0 σ V) o → Term0 σ V (result _ o) := match a with | NoMoreArguments _ y => id | MoreArguments _ x y u q => λ z, apply_args q (z (curry u)) end.
imports: MathClasses.interfaces.canonical_names MathClasses.interfaces.universal_algebra Coq.Program.Program