fact: Definition tail_args x y (a: Arguments (ne_list.cons x y)): Arguments y := match a with | MoreArguments k l m n => n end.
imports: MathClasses.interfaces.canonical_names MathClasses.interfaces.universal_algebra Coq.Program.Program