reorder induction principle

968a2267 · Ralf Jung · 2bc4656d · 968a2267
Commit 968a2267 authored Aug 24, 2017 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 2 deletions

theories/base_logic/fix.v theories/base_logic/fix.v +2 -2

No files found.
--- a/theories/base_logic/fix.v
+++ b/theories/base_logic/fix.v
@@ -40,8 +40,8 @@ Section least.
  Qed.

  Lemma uPred_least_fixpoint_ind (P : A → uPred M) (x : A) :
-    uPred_least_fixpoint F x -∗ □ (∀ y, F P y -∗ P y) -∗ P x.
-  Proof. iIntros "HF #HP". iApply "HF". done. Qed.
+    □ (∀ y, F P y -∗ P y) -∗ uPred_least_fixpoint F x -∗ P x.
+  Proof. iIntros "#HP HF". iApply "HF". done. Qed.
 End least.

 Section greatest.