proposition: Lemma appUnit_left : forall M N (Mapp: isApp M), isAppUnit N (appBodyL Mapp) -> isAppUnit N M.
proof: Proof. intro M; term_inv M. unfold isAppUnit. intros N Mapp. rewrite (appUnits_app Tr Mapp). simpl. auto with datatypes. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)