proposition: Lemma transpose_subs a b : forall u, ~In a (bv u) -> ~In b (bv u) -> transpose a b u = subs (subs_transpose a b) u.
proof: Proof. unfold Def.transpose. induction u; simpl Def.bv; simpl Def.fv; simpl Def.action; set_iff; intros h1 h2. simpl. unfold subs_transpose, Def.transpose_var. eq_dec x a; eq_dec x b; do 2 subst; refl. refl. rewrite IHu1, IHu2; fo. rewrite IHu; [idtac|fo|fo]. assert (h : transpose_var a b x = x). unfold Def.transpose_var. eq_dec x a. fo. eq_dec x b. fo. refl. rewrite h, subs_lam_no_alpha. 2:{ rewrite fvcodom_subs_transpose. eq_dec a b. set_iff. fo. mem. eq_dec x a. fo. eq_dec x b. fo. bool. destruct (mem a (fv u)); destruct (mem b (fv u)); set_iff; fo. } f_equal. rewrite update_id. refl. unfold subs_transpose. rewrite h. refl. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)