Skip to content
Snippets Groups Projects
Commit 49530cb3 authored by Ralf Jung's avatar Ralf Jung
Browse files

rename later_equivI_prop for consistency

parent 56a8f794
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/bi/derived_laws_sbi.v
+ 1
− 1
View file @ 49530cb3
......@@ -172,7 +172,7 @@ Qed.
Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
Proof. apply (anti_symm _); auto using later_eq_1, later_eq_2. Qed.
Lemma later_equivI_prop (P Q : PROP) : ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
Lemma later_equivI_prop_2 (P Q : PROP) : ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
Proof. apply (f_equiv_contractive _). Qed.
(* Later derived *)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment