proposition: Lemma refine_M_hrel_empty : refines M_hrel M.empty M.empty.
proof: Proof. rewrite refinesE; split. { by move=> k; rewrite !F.empty_in_iff. } by move=> k e e' K; exfalso; apply F.empty_mapsto_iff in K. 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)