Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Adam
Iris
Commits
d72f8214
Commit
d72f8214
authored
Sep 26, 2021
by
Ralf Jung
Browse files
fix for f_equiv improvements
parent
467fa48b
Changes
1
Hide whitespace changes
Inline
Side-by-side
iris/bi/internal_eq.v
View file @
d72f8214
...
...
@@ -180,7 +180,6 @@ Lemma discrete_fun_equivI {A} {B : A → ofe} (f g : discrete_fun B) : f ≡ g
Proof
.
apply
(
anti_symm
_
)
;
auto
using
fun_extI
.
apply
(
internal_eq_rewrite'
f
g
(
λ
g
,
∀
x
:
A
,
f
x
≡
g
x
)%
I
)
;
auto
.
intros
n
h
h'
Hh
;
apply
forall_ne
=>
x
;
apply
internal_eq_ne
;
auto
.
Qed
.
Lemma
ofe_morO_equivI
{
A
B
:
ofe
}
(
f
g
:
A
-
n
>
B
)
:
f
≡
g
⊣
⊢
∀
x
,
f
x
≡
g
x
.
Proof
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment