proposition: Lemma shuffle_swap : forall w y n z, w <> z -> y <> z -> (swap w y (swap y z n)) = (swap w z (swap w y n)).
proof: Proof. induction n; intros; simpl; unfold swap_var; default_simp. Qed.
imports: Lia Metalib.Metatheory Metalib.LibLNgen