proposition: Lemma appUnits_notEmpty : forall M hd tl el, appUnits M ++ hd::tl = el::nil -> False.
proof: Proof. intros M hd tl el Eq. destruct (app_eq_unit (appUnits M) (hd::tl) Eq) as [[unitsL argR] | [unitsL argR]]. absurd (appUnits M = nil); auto with terms. discr. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)