fact: Definition mkMatrix2 (v1 v2 v3 v4 : A) := Vcons (vec_of_list (v1 :: v2 :: nil)) (Vcons (vec_of_list (v3 :: v4 :: nil)) Vnil).
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)