Commit 52cc6b15 by Ralf Jung

slightly simplify some proofs in upred.v

parent 3a86d2ff
 ... @@ -341,13 +341,13 @@ Global Instance iff_proper : ... @@ -341,13 +341,13 @@ Global Instance iff_proper : (** Introduction and elimination rules *) (** Introduction and elimination rules *) Lemma const_intro φ P : φ → P ⊑ ■ φ. Lemma const_intro φ P : φ → P ⊑ ■ φ. Proof. by intros ?? [|?]. Qed. Proof. by intros ???. Qed. Lemma const_elim φ Q R : Q ⊑ ■ φ → (φ → Q ⊑ R) → Q ⊑ R. Lemma const_elim φ Q R : Q ⊑ ■ φ → (φ → Q ⊑ R) → Q ⊑ R. Proof. intros HQP HQR x n ??; apply HQR; first eapply (HQP _ n); eauto. Qed. Proof. intros HQP HQR x n ??; apply HQR; first eapply (HQP _ n); eauto. Qed. Lemma True_intro P : P ⊑ True. Lemma True_intro P : P ⊑ True. Proof. by apply const_intro. Qed. Proof. by apply const_intro. Qed. Lemma False_elim P : False ⊑ P. Lemma False_elim P : False ⊑ P. Proof. by intros x [|n] ?. Qed. Proof. by intros x n ?. Qed. Lemma and_elim_l P Q : (P ∧ Q) ⊑ P. Lemma and_elim_l P Q : (P ∧ Q) ⊑ P. Proof. by intros x n ? [??]. Qed. Proof. by intros x n ? [??]. Qed. Lemma and_elim_r P Q : (P ∧ Q) ⊑ Q. Lemma and_elim_r P Q : (P ∧ Q) ⊑ Q. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!