proposition: Lemma transpose_sym x y : forall u, transpose x y u = transpose y x u.
proof: Proof. unfold Def.transpose. induction u; simpl. rewrite transpose_var_sym. refl. refl. rewrite IHu1, IHu2. refl. rewrite IHu, transpose_var_sym, transpose_var_sym with (x:=y). refl. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)