From 6f629be03128cb67309c10f29afa25b45e0cddc1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Aug 2017 16:09:17 +0200
Subject: [PATCH] move quantifiers

---
 theories/base_logic/fix.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/base_logic/fix.v b/theories/base_logic/fix.v
index cbecbdc10..e8f89d6c6 100644
--- a/theories/base_logic/fix.v
+++ b/theories/base_logic/fix.v
@@ -20,7 +20,7 @@ Section least.
 
   Lemma F_fix_implies_least_fixpoint x : F (uPred_least_fixpoint F) x ⊢ uPred_least_fixpoint F x.
   Proof.
-    iIntros "HF" (P). iApply wand_impl_always. iIntros "#Hincl".
+    iIntros "HF" (P) "#Hincl".
     iApply "Hincl". iApply (Hmono _ P); last done.
     iIntros "!#" (y) "Hy". iApply "Hy". done.
   Qed.
@@ -39,9 +39,9 @@ Section least.
     apply (anti_symm _); auto using least_fixpoint_implies_F_fix, F_fix_implies_least_fixpoint.
   Qed.
 
-  Lemma uPred_least_fixpoint_ind (P : A → uPred M) (x : A) :
-    □ (∀ y, F P y -∗ P y) -∗ uPred_least_fixpoint F x -∗ P x.
-  Proof. iIntros "#HP HF". iApply "HF". done. Qed.
+  Lemma uPred_least_fixpoint_ind (P : A → uPred M) :
+    □ (∀ y, F P y -∗ P y) -∗ ∀ x, uPred_least_fixpoint F x -∗ P x.
+  Proof. iIntros "#HP" (x) "HF". iApply "HF". done. Qed.
 End least.
 
 Section greatest.
@@ -70,7 +70,7 @@ Section greatest.
     apply (anti_symm _); auto using greatest_fixpoint_implies_F_fix, F_fix_implies_greatest_fixpoint.
   Qed.
 
-  Lemma uPred_greatest_fixpoint_coind (P : A → uPred M) (x : A) :
-    □ (∀ y, P y -∗ F P y) -∗ P x -∗ uPred_greatest_fixpoint F x.
-  Proof. iIntros "#HP Hx". iExists P. by iIntros "{$Hx} !#". Qed.
+  Lemma uPred_greatest_fixpoint_coind (P : A → uPred M) :
+    □ (∀ y, P y -∗ F P y) -∗ ∀ x, P x -∗ uPred_greatest_fixpoint F x.
+  Proof. iIntros "#HP" (x) "Hx". iExists P. by iIntros "{$Hx} !#". Qed.
 End greatest.
-- 
GitLab