proposition: Lemma refine_M_hrel_map : refines ((rAC ==> rAC) ==> M_hrel ==> M_hrel) (@M.map A A) (@M.map C C).
proof: Proof. apply refines_abstr => f f' ref_f. apply refines_abstr => m m' ref_m. rewrite refinesE; split. { move=> k; rewrite !F.map_in_iff. move: ref_m; rewrite refinesE => H'; apply H'. } move=> k e e' H1 H2. apply map_mapsto_iff_dec in H1. apply map_mapsto_iff_dec in H2. move: H1 H2 => [a Ha] [a' Ha']. rewrite (proj1 Ha) (proj1 Ha'). apply refinesP; eapply refines_apply; [by apply ref_f|]. move: ref_m (proj2 Ha) (proj2 Ha'); rewrite !refinesE => ref_m. apply (snd ref_m). Qed.
imports: ZArith NArith FMaps FMapAVL mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice finfun tuple fintype ssralg bigop) CoqEAL(hrel) CoqEAL(refinements) CoqEAL(param binord binnat) CoqEAL(seqmx ) CoqEAL(ssrcomplements) mathcomp.multinomials(mpoly freeg)