proposition: Lemma map2_correct : forall sv1 sv2 st1 st2, RelP sv1 st1 -> RelP sv2 st2 -> RelP (map2 vop vop' sv1 sv2) (map2 top top' st1 st2).
proof: Proof. Proof using H0 H0t H0v Hop' H0eq H0t1 H0t2 H0v1 H0v2 Hop. move=> sv1 sv2 st1 st2 H1 H2 k; move/(_ k) in H1; move/(_ k) in H2. rewrite !nth_map2_dflt. do 4![case:ifP]=> A B C D; rewrite ?(nth_default _ A) ?(nth_default _ B) ?(nth_default _ C) ?(nth_default _ D) // in H1 H2; try solve [exact: H0t1|exact: H0t2|exact: H0v1|exact: H0v2|exact: Hop'|exact: Hop|exact: H0t|exact: H0v]. - rewrite (H0eq (H0t H2)); exact: H1. - rewrite (H0eq H1); apply: H0v; exact: H2. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2