fact: Definition absBody M : isAbs M -> Term := match M return (isAbs M -> Term) with | buildT typ => match typ return (isAbs (buildT typ) -> Term) with | TAbs absT => fun _ : True => buildT absT | _ => fun notAbs: False => False_rect Term notAbs end end.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)