proposition: Lemma mat_forall2'_dec : rel_dec mat_forall2'.
proof: Proof. intros M N. unfold mat_forall2'. do 2 apply Vforall2_dec. hyp. Defined.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)