Make [ELCtx_Alive] a coercion

I made ELCtx_Alive a coercion.

This has several consequences:

• lft has to be a definition instead of a notation. In order to make sure that it will not be unfolded, I made it part of the signature of the lifetime logic
• The parameters of the fn type have to be uncurried, so that the type inference of Coq determines the value of A befor type-checking the external lifetime environment.

What do you think? Is it worth merging as-is or should we use a notation after all?

theories/lifetime/model/borrow.v

@@ -136,9 +136,9 @@ Lemma bor_combine E κ P Q :
 Proof.
   iIntros (?) "#LFT HP HQ". rewrite {1 2}/bor.
   iDestruct "HP" as (κ1) "[#Hκ1 Hbor1]". iDestruct "HQ" as (κ2) "[#Hκ2 Hbor2]".
-  iMod (raw_rebor _ _ (κ1 ∪ κ2) with "LFT Hbor1") as "[Hbor1 _]".
+  iMod (raw_rebor _ _ (κ1 ⊓ κ2) with "LFT Hbor1") as "[Hbor1 _]".
     done. by apply gmultiset_union_subseteq_l.
-  iMod (raw_rebor _ _ (κ1 ∪ κ2) with "LFT Hbor2") as "[Hbor2 _]".
+  iMod (raw_rebor _ _ (κ1 ⊓ κ2) with "LFT Hbor2") as "[Hbor2 _]".
     done. by apply gmultiset_union_subseteq_r.
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". unfold raw_bor, idx_bor_own.
   iDestruct "Hbor1" as (j1) "[Hbor1 Hslice1]". iDestruct "Hbor2" as (j2) "[Hbor2 Hslice2]".
@@ -177,7 +177,7 @@ Proof.
                 -fmap_None -lookup_fmap !fmap_delete //. }
     rewrite own_bor_op. iDestruct "Hbor" as "[H● H◯]".
     iAssert (&{κ}(P ∗ Q))%I with "[H◯ Hslice]" as "$".
-    { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ∪ κ2).
+    { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ⊓ κ2).
       iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2").
       iExists γ. iFrame. iExists _. iFrame. iNext. iAlways.
       by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }