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