Commit a9c5bc54 authored by Ralf Jung's avatar Ralf Jung
Browse files

simplify an inG proof

parent c4d8c28a
......@@ -18,7 +18,7 @@ Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Proof. intros ?%subG_inG. split; apply _. Qed.
Section proof.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
Supports Markdown
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