fact: Fixpoint app_tree {V} {o}: Term V o → op_type (Term0 V) o := match o with | ne_list.one _ => id | ne_list.cons _ _ => λ x y, app_tree (App _ _ _ x y) end.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.misc.util MathClasses.theory.jections MathClasses.interfaces.ua_basic