fact: Fixpoint ComputableS (M: Term) (T: SimpleType) : Prop := algebraic M /\ type M = T /\ match T with | #T => AccR M | TL --> TR => forall P (Papp: isApp P) (PL: (appBodyL Papp) ~ M) (typeL: type P = TR) (typeR: type (appBodyR Papp) = TL), algebraic (appBodyR Papp) -> ComputableS (appBodyR Papp) TL -> ComputableS P TR end.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)