proposition: Lemma appUnit_subterm : forall M N, isApp M -> isAppUnit N M -> subterm N M.
proof: Proof. destruct M as [E Pt A TypM]. induction TypM; try contr. intros N M1M2app Narg. case (isApp_dec (buildT TypM1)). intro M1app. unfold isAppUnit in Narg. rewrite (appUnits_app (buildT (TApp TypM1 TypM2)) M1M2app) in Narg. simpl in Narg. case (@in_app_or _ (appUnits (buildT TypM1)) (buildT TypM2::nil) N). trivial. constructor 1 with M1M2app; constructor. apply IHTypM1; trivial. intro N_M2. constructor 2 with M1M2app. inversion N_M2. rewrite <- H; constructor 2. contr. intro M1notApp. unfold isAppUnit, appUnits in Narg. simpl in Narg. change TypM1 at 2 with (typing (buildT TypM1)) in Narg. fold (appUnits (buildT TypM1)) in Narg. case (@in_app_or _ (appUnits (buildT TypM1)) (buildT TypM2::nil) N). trivial. intro N_M1; constructor 1 with M1M2app. rewrite appUnits_notApp in N_M1; trivial. destruct (in_inv N_M1) as [NM1 | Nnil]. rewrite <- NM1; constructor 2. absurd (In N nil); auto with datatypes. intro N_M2; constructor 2 with M1M2app. destruct (in_inv N_M2) as [NM2 | Nnil]. rewrite <- NM2; constructor 2. absurd (In N nil); auto with datatypes. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)