Commit 7378a401 by Robbert Krebbers

### Simplify another proof.

parent 8c13c02f
 ... @@ -94,10 +94,7 @@ Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A -n> iProp Σ) ... @@ -94,10 +94,7 @@ Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A -n> iProp Σ) saved_anything_own (F := A -n> ▶ ∙) γ (CofeMor Next ◎ Φ). saved_anything_own (F := A -n> ▶ ∙) γ (CofeMor Next ◎ Φ). Instance saved_pred_own_contractive `{savedPredG Σ A} γ : Contractive (saved_pred_own γ). Instance saved_pred_own_contractive `{savedPredG Σ A} γ : Contractive (saved_pred_own γ). Proof. Proof. rewrite /saved_pred_own=> n Φ Φ' ?. f_equiv=> x /=. by f_contractive. Qed. intros n Φ Φ' HΦ. rewrite /saved_pred_own /saved_anything_own /=. do 3 f_equiv. intros x. rewrite /=. by f_contractive. Qed. Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A -n> iProp Σ) : Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A -n> iProp Σ) : (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ Φ)%I. (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ Φ)%I. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!