proposition: Lemma comp_units_comp : forall M, (forall N, isAppUnit N M -> Computable N) -> Computable M.
proof: Proof. destruct M as [E Pt T TypM]; induction TypM; intro compUnits; try solve [apply compUnits; compute; auto]. apply comp_app with I; simpl. apply IHTypM1. intros N NunitL; apply compUnits. apply appUnit_left with I; trivial. apply compUnits. red. rewrite (appUnits_app (buildT (TApp TypM1 TypM2)) I). auto with datatypes. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)