proposition: Lemma app_notApp_diffUnits : forall M N, isApp M -> ~isApp N -> appUnits M = appUnits N -> False.
proof: Proof. intros M N Mapp Nnapp eqUnits. rewrite (appUnits_app M Mapp) in eqUnits. rewrite (appUnits_notApp N Nnapp) in eqUnits. eapply appUnits_notEmpty; eexact eqUnits. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)