proposition: Lemma mat_forall2_dec : rel_dec mat_forall2.
proof: Proof. intros M N. destruct (mat_forall2'_dec M N). left. apply mat_forall2_equiv2. hyp. right. intro. apply n0. apply mat_forall2_equiv1. hyp. Defined.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)