proposition: Lemma fvcodom_subs_transpose a b xs : fvcodom xs (subs_transpose a b) [=] if eqb a b then empty else union (if mem a xs then singleton b else empty) (if mem b xs then singleton a else empty).
proof: Proof. unfold Def.fvcodom. rewrite domain_subs_transpose. eq_dec a b. rewrite fvcod_empty. refl. rewrite fvcod_subs_transpose. mem. bool. rewrite !remove_inter, <- remove_add_com. 2: hyp. rewrite remove_singleton, remove_add_eq, remove_empty, inter_empty_r, union_empty_l. refl. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)