proposition: Lemma swap_this : forall T (Mpos: PlaceHolder (PThis T)) (M := proj1_sig2 Mpos), swap Mpos = M.
proof: Proof. intros; apply term_eq. rewrite swap_env_eq; trivial. destruct Mpos; unfold M; simpl. rewrite <- e; trivial. rewrite swap_term_is; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsBuilding)