Commit 53c8c569 authored by Ralf Jung's avatar Ralf Jung

some missing fixes

parent c5f21766
......@@ -94,7 +94,7 @@ Section Rules.
Proof.
iIntros "[Howns Hls] Hl".
iDestruct (own_valid_2 with "Howns Hl")
as %[[az [Haz Hq]]%singleton_included _]%auth_both_valid.
as %[[az [Haz Hq]]%singleton_included_l _]%auth_both_valid.
rewrite lookup_fmap in Haz.
assert ( z, h !! l = Some z) as Hz.
{ revert Haz; case: (h !! l) => [z|] Hz; first (by eauto); inversion Hz. }
......
......@@ -113,7 +113,7 @@ Section conversions.
Lemma tpool_singleton_included tp j e :
{[j := Excl e]} to_tpool tp tp !! j = Some e.
Proof.
move=> /singleton_included [ex [/leibniz_equiv_iff]].
move=> /singleton_included_l [ex [/leibniz_equiv_iff]].
rewrite tpool_lookup fmap_Some=> [[e' [-> ->]] /Excl_included ?]. by f_equal.
Qed.
Lemma tpool_singleton_included' tp j e :
......
......@@ -356,7 +356,7 @@ Section graph.
apply: map_eq => i. apply leibniz_equiv, equiv_dist => n.
destruct (decide (x = i)); subst;
rewrite ?lookup_insert ?lookup_insert_ne //.
apply singleton_included in H12. destruct H12 as [y [H31 H32]].
apply singleton_included_l in H12. destruct H12 as [y [H31 H32]].
rewrite H31 (Some_included_exclusive _ _ H32); try done.
destruct H2 as [H21 H22]; simpl in H22.
specialize (H22 i); revert H22; rewrite H31; done.
......
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