proposition: Lemma swap_not_funApp : forall T (pos: Pos T) (Mpos: PlaceHolder pos) (M := proj1_sig2 Mpos), pos <> PThis T -> ~isFunApp T -> (isFunApp M -> isBaseType (type M)) -> ~isFunApp (swap Mpos).
proof: Proof. induction pos; intros; try_solve. assert (isAbs (swap Mpos)). apply swap_abs. unfold isFunApp; rewrite appHead_notApp; term_inv (swap Mpos). assert (MPapp: isApp (swap Mpos)). apply app_swap_app; simpl; trivial. apply notFunApp_left with MPapp. destruct (placeHolder_appL Mpos) as [MPin MPeq]. rewrite <- (swap_in_appL MPin Mpos); trivial. destruct (posThis_dec pos). replace (swap MPin) with M. intro Mfa. absurd (isBaseType (type M)). unfold M; destruct Mpos; simpl in * . rewrite <- e1; rewrite e; auto. apply H1; trivial. apply term_eq. rewrite swap_env_eq; trivial. unfold M; destruct MPin; simpl in * . rewrite <- MPeq; rewrite <- e0; rewrite e; trivial. rewrite swap_term_is; trivial. rewrite MPeq. unfold M; destruct Mpos; simpl in * . rewrite e; trivial. apply IHpos; try_solve. change (buildT AppL) with (appBodyL (M:=buildT (TApp AppL AppR)) I). apply notFunApp_left_inv; trivial. rewrite MPeq; trivial. assert (MPapp: isApp (swap Mpos)). apply app_swap_app; simpl; trivial. apply notFunApp_left with MPapp. destruct (placeHolder_appR Mpos). rewrite (appBodyL_swap_in_appR x Mpos MPapp); trivial. change (buildT AppL) with (appBodyL (M:=buildT (TApp AppL AppR)) I). apply notFunApp_left_inv; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsBuilding)