From 1190a3218be26b1510a97c81f475e45f502f3d22 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 Apr 2016 17:20:56 +0200
Subject: [PATCH] Prove False_elim in logic instead of model.

---
 algebra/upred.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index e0a9e313f..9b1a2ffef 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -467,8 +467,6 @@ Lemma const_elim φ Q R : Q ⊢ ■ φ → (φ → Q ⊢ R) → Q ⊢ R.
 Proof.
   unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
 Qed.
-Lemma False_elim P : False ⊢ P.
-Proof. by unseal; split=> n x ?. Qed.
 Lemma and_elim_l P Q : (P ∧ Q) ⊢ P.
 Proof. by unseal; split=> n x ? [??]. Qed.
 Lemma and_elim_r P Q : (P ∧ Q) ⊢ Q.
@@ -512,6 +510,8 @@ Proof.
 Qed.
 
 (* Derived logical stuff *)
+Lemma False_elim P : False ⊢ P.
+Proof. by apply (const_elim False). Qed.
 Lemma True_intro P : P ⊢ True.
 Proof. by apply const_intro. Qed.
 Lemma and_elim_l' P Q R : P ⊢ R → (P ∧ Q) ⊢ R.
-- 
GitLab