Proofs about binders

Now that POPL deadline is over, here are some more lemmata. As always let me know if I should change anything.

theories/binders.v

@@ -42,8 +42,39 @@ Proof.
   constructor. rewrite <-(set_unfold (x ∈ X) P).
   destruct mx; simpl; rewrite ?elem_of_cons; naive_solver.
 Qed.
-Instance set_unfold_app_binder x mxl X P :
-  SetUnfoldElemOf x X P → SetUnfoldElemOf x (mxl +b+ X) (BNamed x ∈ mxl ∨ P).
+Instance set_unfold_app_binder x mxl X P Q :
+  SetUnfoldElemOf x X P → SetUnfoldElemOf (BNamed x) mxl Q → SetUnfoldElemOf x (mxl +b+ X) (Q ∨ P).
 Proof.
-  constructor. rewrite <-(set_unfold (x ∈ X) P). induction mxl; set_solver.
+  intros HinX HinQ.
+  constructor. rewrite <-(set_unfold (x ∈ X) P), <-(set_unfold (BNamed x ∈ mxl) Q).
+  clear HinX HinQ.
+  induction mxl; set_solver.
+Qed.
+
+Lemma app_binder_named mxl xl : (BNamed <$> mxl) +b+ xl = mxl ++ xl.
+Proof. induction mxl; csimpl; eauto with f_equal. Qed.
+
+Lemma app_binder_tail_cons l1 x l2 : l1 +b+ (x :: l2) = (l1 ++ [BNamed x]) +b+ l2.
+Proof. induction l1; csimpl; eauto with f_equal. Qed.
+
+Lemma Permutation_app_binder_head l1 l2 l :
+  l1 ≡ₚ l2 → l1 +b+ l ≡ₚ l2 +b+ l.
+Proof.
+  induction 1 as [|[] [] []|[] []|]; csimpl; eauto using Permutation_trans.
+  by rewrite perm_swap.
+Qed.
+
+Lemma Permutation_app_binder_tail l1 l2 l :
+  l1 ≡ₚ l2 → l +b+ l1 ≡ₚ l +b+ l2.
+Proof.
+  intros Hperm. revert l.
+  induction Hperm as [| | |]; eauto using Permutation_trans; intros ?.
+  - by rewrite app_binder_tail_cons, app_binder_tail_cons, Permutation_app_binder_head.
+  - rewrite app_binder_tail_cons, app_binder_tail_cons, app_binder_tail_cons, app_binder_tail_cons, Permutation_app_binder_head; try done.
+    by rewrite <-Permutation_cons_append, <-Permutation_cons_append, <-Permutation_cons_append, <-Permutation_cons_append, perm_swap.
+Qed.
+
+Instance app_binder_proper_perm : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡ₚ)) app_binder.
+Proof.
+  intros ????. eauto using Permutation_trans, Permutation_app_binder_head, Permutation_app_binder_tail.
 Qed.