proposition: Lemma app_swap_app : forall M (pos: Pos M) (MP: PlaceHolder pos), pos <> PThis M -> isApp M -> isApp (swap MP).
proof: Proof. destruct pos; intros; try_solve. eapply app_isApp. rewrite swap_term_is; simpl; eauto. eapply app_isApp. rewrite swap_term_is; simpl; eauto. Qed.
imports: CoLoR(RelExtras ListExtras TermsBuilding)