proposition: Lemma appUnits_not_nil : forall M, appUnits M <> nil.
proof: Proof. destruct M as [E Pt A TypM]. induction TypM; solve [unfold appUnits; simpl; auto with datatypes]. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)