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

make a proof script slightly more robust

parent 1d312d31
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/algebra/functions.v
+ 1
− 1
View file @ 11bb8eb2
...@@ -150,7 +150,7 @@ Section cmra. ...@@ -150,7 +150,7 @@ Section cmra.
exists (discrete_fun_singleton x y2); split; [by apply HQ|]. exists (discrete_fun_singleton x y2); split; [by apply HQ|].
intros x'; destruct (decide (x' = x)) as [->|]. intros x'; destruct (decide (x' = x)) as [->|].
- by rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton. - by rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton.
- rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton_ne //. apply Hg. - rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton_ne //; by apply Hg.
Qed. Qed.
Lemma discrete_fun_singleton_updateP_empty' x (P : B x → Prop) : Lemma discrete_fun_singleton_updateP_empty' x (P : B x → Prop) :
ε ~~>: P → ε ~~>: λ g, ∃ y2, g = discrete_fun_singleton x y2 ∧ P y2. ε ~~>: P → ε ~~>: λ g, ∃ y2, g = discrete_fun_singleton x y2 ∧ P y2.
......
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