proposition: Lemma appUnit_right : forall M N (Mapp: isApp M), N = appBodyR Mapp -> isAppUnit N M.
proof: Proof. intros. unfold isAppUnit. rewrite H. rewrite (appUnits_app M Mapp). auto with datatypes. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)