fact: Definition appBodyL M : isApp M -> Term := match M return (isApp M -> Term) with | buildT typ => match typ return (isApp (buildT typ) -> Term) with | TApp L R => fun _ : True => buildT L | _ => fun notApp: False => False_rect Term notApp end end.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)