proposition: Lemma bvcod_fun_transp s : transpose Equal (bvcod_fun s).
proof: Proof. intros u v vs. unfold bvcod_fun. intro a. set_iff. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)