fact: Definition huncurry {As B} (f : himpl As B) (xs : hlist As) : B := (fix go {As} xs := match xs in hlist As return himpl As B → B with | hnil => λ f, f | hcons x xs => λ f, go xs (f x) end) _ xs f.
imports: stdpp(tactics) stdpp(options)