proposition: Lemma fvcod_subs_transpose a b : forall xs, fvcod xs (subs_transpose a b) [=] union (remove a (remove b xs)) (union (if mem a xs then singleton b else empty) (if mem b xs then singleton a else empty)).
proof: Proof. apply set_induction_bis. intros xs xs' xsxs'. rewrite xsxs'. auto. mem. rewrite fvcod_empty. intro; set_iff; tauto. intros x xs n IH. rewrite fvcod_add, IH. 2: hyp. mem. unfold Def.fvcod_fun. ens. rewrite remove_add_if, eqb_sym. unfold subs_transpose, Def.transpose_var, eqb. eq_dec x a; eq_dec x b; do 2 subst; simpl. rewrite !union_idem, !remove_idem. destruct (mem b xs); intro; set_iff; tauto. rewrite not_mem_iff in n. rewrite n, remove_add_eq, union_empty_l, union_sym_2. refl. rewrite not_mem_iff in n. rewrite n. destruct (mem a xs); intro; set_iff; tauto. rewrite remove_add_if. eq_dec a x. subst. cong. rewrite add_union_singleton, union_assoc. refl. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)