fact: Fixpoint applications {ot}: Term V ot → Type := match ot with | ne_list.one x => @P x | ne_list.cons x y => λ z, ∀ v, P v → applications (App V _ _ z v) end.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.misc.util MathClasses.theory.jections MathClasses.interfaces.ua_basic