proposition: Lemma appUnit_notApp : forall M Mu, isAppUnit Mu M -> ~isApp M -> Mu = M.
proof: Proof. intros. unfold isAppUnit in H. rewrite appUnits_notApp in H; trivial. inversion H; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)