proposition: Lemma swap_equivariance : forall t x y z w, swap x y (swap z w t) = swap (swap_var x y z) (swap_var x y w) (swap x y t).
proof: Proof. induction t; intros; simpl. - rewrite swap_var_equivariance. auto. - rewrite swap_var_equivariance. rewrite IHt. auto. - rewrite IHt1. rewrite IHt2. auto. Qed.
imports: Lia Metalib.Metatheory Metalib.LibLNgen