proposition: Lemma mat_forall2_equiv1 : forall M N, mat_forall2 M N -> mat_forall2' M N.
proof: Proof. intros. unfold mat_forall2'. do 2 (apply Vforall2_intro_nth; intros). exact (H i i0 ip ip0). Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)