proposition: Lemma map_correct : forall sv st, RelP sv st -> RelP (map vop sv) (map top st).
proof: Proof. move=> sv st Hnth k; move/(_ k) in Hnth. rewrite !nth_map_dflt. do 2![case:ifP]=> A B //; rewrite ?(nth_default _ A) ?(nth_default _ B) in Hnth. - exact: H0v. - exact: H0t. - exact: Hop. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2