proposition: Lemma transpose_var_com a b c d z : a <> c -> a <> d -> b <> c -> b <> d -> transpose_var a b (transpose_var c d z) = transpose_var c d (transpose_var a b z).
proof: Proof. intros nac nad nbc nbd. unfold Def.transpose_var. eq_dec z c; subst. eq_dec d a; subst. cong. eq_dec d b; subst. cong. eq_dec c a; subst. cong. eq_dec c b; subst. cong. eq_dec c c; subst. refl. cong. eq_dec z d; subst. eq_dec c a; subst. cong. eq_dec c b; subst. cong. eq_dec d a; subst. cong. eq_dec d b; subst. cong. eq_dec d c; subst. refl. eq_dec d d; subst. refl. cong. eq_dec z a; subst. eq_dec b c; subst. cong. eq_dec b d; subst. cong. refl. eq_dec z b; subst. eq_dec a c; subst. cong. eq_dec a d; subst. cong. refl. eq_dec z c; subst. cong. eq_dec z d; subst. cong. refl. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)