proposition: Lemma transpose_comp a b c : forall u, ~In b (fv u) -> ~In b (bv u) -> ~In c (fv u) -> ~In c (bv u) -> transpose b c (transpose a b u) = transpose a c u.
proof: Proof. unfold Def.transpose. induction u; simpl; set_iff; intros h1 h2 h3 h4; f_equal; try apply transpose_var_comp; fo. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)