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