fact: Definition neutral (u : Te) := match u with | Def.Lam _ _ => False | _ => match head u with | Def.Fun _ => False | _ => True end end.
imports: Coq(Morphisms Basics Lia) CoLoR(LogicUtil RelUtil VecOrd VecUtil LAlpha)