proposition: Lemma transpose_var_comp a b c z : b <> z -> c <> z -> transpose_var b c (transpose_var a b z) = transpose_var a c z.
proof: Proof. intros nbz ncz. unfold Def.transpose_var. eq_dec z a; subst. eq_dec b b; subst. refl. cong. eq_dec z b; subst. cong. eq_dec z b; subst. cong. eq_dec z c; subst. cong. refl. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)