Commit 9271f6e3 authored by Robbert Krebbers's avatar Robbert Krebbers

More consistent name of projection for `AsEmpValid0` class.

parent 0d07104f
......@@ -498,9 +498,9 @@ Class AsEmpValid {PROP : bi} (φ : Prop) (P : PROP) :=
as_emp_valid : φ bi_emp_valid P.
Arguments AsEmpValid {_} _%type _%I.
Class AsEmpValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
as_emp_valid_here : AsEmpValid φ P.
as_emp_valid_0 : AsEmpValid φ P.
Arguments AsEmpValid0 {_} _%type _%I.
Existing Instance as_emp_valid_here | 0.
Existing Instance as_emp_valid_0 | 0.
Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
φ bi_emp_valid P.
......
Markdown is supported
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