proposition: Lemma swap_var_equivariance : forall v x y z w, swap_var x y (swap_var z w v) = swap_var (swap_var x y z) (swap_var x y w) (swap_var x y v).
proof: Proof. unfold swap_var; default_simp. Qed.
imports: Lia Metalib.Metatheory Metalib.LibLNgen