proposition: Lemma appUnit_head_or_arg : forall M M', In M' (appUnits M) -> M' = appHead M \/ In M' (appArgs M).
proof: Proof. intros. destruct (in_head_tail M' (appUnits M) H). left; sym. unfold appHead; apply head_of_notNil; auto. right; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)