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