proposition: Lemma swap_isFunApp : forall T (pos: Pos T) (Mpos: PlaceHolder pos) (M := proj1_sig2 Mpos), isFunApp T -> ~isFunApp (T // pos) -> isFunApp (swap Mpos).
proof: Proof. induction pos; try_solve; intros. set (MPapp := swap_left_app Mpos). unfold isFunApp in * . rewrite (appHead_app (swap Mpos) MPapp). destruct (placeHolder_appL Mpos). replace (appBodyL MPapp) with (swap x). apply IHpos; trivial. rewrite (@appHead_app (buildT (TApp AppL AppR)) I) in H; trivial. apply term_eq. rewrite appBodyL_env, !swap_env_eq; trivial. rewrite (@appBodyL_term (swap Mpos) (swap_term pos (proj1_sig2 Mpos)) PtR); trivial. rewrite swap_term_is, e; trivial. rewrite swap_term_is; trivial. set (MPapp := swap_right_app Mpos). unfold isFunApp in * . rewrite (appHead_app (swap Mpos) MPapp). destruct (placeHolder_appR Mpos). rewrite (@appBodyL_swap_in_appR E PtL PtR A B AppL AppR pos Mpos Mpos); trivial. rewrite (@appHead_app (buildT (TApp AppL AppR)) I) in H; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsBuilding)