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