fact: Record appCond : Type := { appL: Term; appR: Term; eqEnv: env appL = env appR; typArr: isArrowType (type appL); typOk: type_left (type appL) = type appR }.
imports: CoLoR(RelExtras ListExtras LogicUtil) Coq(Lia)