proposition: Lemma appArg_inv : forall M N (Mapp: isApp M), isArg N M -> (isArg N (appBodyL Mapp) \/ N = (appBodyR Mapp)).
proof: Proof. destruct M as [E Pt A typM]. induction typM; simpl; intros; try contr. unfold isArg in H. rewrite (appArgs_app (buildT (TApp typM1 typM2)) Mapp) in H. case (@in_app_or _ (appArgs (buildT typM1)) (buildT typM2::nil) N); auto. destruct 1; solve [auto | contr]. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)