proposition: Lemma refine_M_hrel_fold : refines ((eq ==> rAC ==> M_hrel ==> M_hrel) ==> M_hrel ==> M_hrel ==> M_hrel) (@M.fold A _) (@M.fold C _).
proof: Proof. apply refines_abstr => f f' ref_f. apply refines_abstr => m m' ref_m. apply refines_abstr => i i' ref_i. move: (refines_apply refine_M_hrel_elements ref_m); rewrite !M.fold_1 !refinesE. move: i i' ref_i; generalize (M.elements m), (M.elements m'). elim=> [|h t IHt]; case=> //=. - by move=> i i'; rewrite refinesE. - by move=> a l i i' _ K; inversion K. - by move=> i i' _ K; inversion K. move=> h' t' i i' ref_i Hyp. eapply inv_list_R; last exact: Hyp; try done. move=> H a c sa sc Heq Heqs [H1 H2] [H3 H4]. apply: IHt; last first. rewrite -H2 -H4; exact: Heqs. rewrite -H1 -H3; case: Heq => [h1 _ <- h2 h2' rh2] /=. apply: refines_apply ref_i. apply: refines_apply. apply: refines_apply. by rewrite refinesE. 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)