From 968a2267924500fd0a9f36b0778a998ea064e104 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 24 Aug 2017 16:07:18 +0200 Subject: [PATCH] reorder induction principle --- theories/base_logic/fix.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/base_logic/fix.v b/theories/base_logic/fix.v index 717845fbc..cbecbdc10 100644 --- 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. -- GitLab