fact: Fixpoint forallArgs {o} (a: Arguments o): Type := match a with | NoMoreArguments _ => True | MoreArguments _ _ z v => prod (P z) (forallArgs v) end.
imports: MathClasses.interfaces.canonical_names MathClasses.interfaces.universal_algebra Coq.Program.Program