proposition: Lemma domain_subs_transpose a b : forall xs, domain xs (subs_transpose a b) [=] if eqb a b then empty else inter xs (add a (singleton b)).
proof: Proof. apply set_induction_bis. intros xs xs' xsxs'. destruct (eqb a b); rewrite xsxs'; auto. rewrite domain_empty. destruct (eqb a b). refl. rewrite inter_empty_l. refl. intros x xs n IH. rewrite domain_add, IH. 2: hyp. unfold Def.domain_fun. ens. unfold subs_transpose, Def.transpose_var. rewrite beq_term_var. eq_dec x a. subst. eq_dec a b; eq_dec b a. refl. firstorder auto with exfalso. firstorder auto with exfalso. intro; set_iff; tauto. eq_dec x b. subst. eq_dec a b. refl. intro; set_iff; tauto. eq_dec x x. 2: cong. eq_dec a b. refl. intro y. set_iff. split_all; subst; cong. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)