Skip to content
Snippets Groups Projects
Commit 79df624d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Small clean up.

parent 66904606
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/joining_existentials.v
+ 2
− 2
View file @ 79df624d
...@@ -57,8 +57,8 @@ Proof. ...@@ -57,8 +57,8 @@ Proof.
{ iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'". { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
rewrite own_valid csum_validI /= agree_validI agree_equivI later_equivI /=. rewrite own_valid csum_validI /= agree_validI agree_equivI later_equivI /=.
rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id. rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
rewrite (ne_proper (cFunctor_map G) (cid, cid) (_ ◎ _, _ ◎ _)). rewrite (ne_proper (cFunctor_map G) (cid, cid) (_ ◎ _, _ ◎ _)); last first.
2:by split; intro; simpl; symmetry; apply iProp_fold_unfold. { by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". } rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". }
iNext. iRewrite -"Hxx" in "Hx'". iNext. iRewrite -"Hxx" in "Hx'".
iExists x; iFrame "Hγ". iApply Ψ_join; by iSplitL "Hx". iExists x; iFrame "Hγ". iApply Ψ_join; by iSplitL "Hx".
......
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