Add more lemmas for gmap uncurry

mentioned in commit FP/promising@1d375f24

mentioned in commit 6f1a23cb

merged

gmap_uncurry_nonempty could be proved in an easier way using gmap_uncurry_None, see https://gitlab.mpi-sws.org/FP/gpfsl/blob/master/theories/lang/history.v#L11.

The page could not be found or you don't have permission to view it.

Lemma gmap_uncurry_nonempty `{Countable K1, Countable K2} {A : Type}
    (m : gmap (K1 * K2) A):
  ∀ i x, gmap_uncurry m !! i = Some x → x ≠ ∅.
Proof.
  intros ?? EMP ->. eapply eq_None_not_Some; last by eexists.
  eapply lookup_gmap_uncurry_None=>?. rewrite -lookup_gmap_uncurry EMP //.
Qed.

The project is private and I have no permission to change it. Added @robbertkrebbers to that project.

I can make gpfsl (and promising) public if you want.

Yeah, only owners of the FP group can make the project public. Cc @jung.

@jung yes please make it public. Thanks.

mentioned in commit c53cefcd

@jjourdan thanks, I ported your shortened proof to vanilla Coq and added it.

gpfsl is public now.