proposition: Lemma transpose_var_sym x y z : transpose_var x y z = transpose_var y x z.
proof: Proof. unfold Def.transpose_var. eq_dec z x; eq_dec z y; subst; auto. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)