NIT

logsem · Sep 26, 2024 · 95f38e6 · 95f38e6
1 parent 9200128
commit 95f38e6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/coneris/examples/random_counter/random_counter.v b/theories/coneris/examples/random_counter/random_counter.v
@@ -136,7 +136,7 @@ Section lemmas.
             (λ ε α' ε2 num ns ns',
                ∃ n z, 
                  ⌜num=1%nat⌝ ∗ ⌜α'=α⌝ ∗ ⌜ns=[]⌝ ∗ ⌜ns'=[n]⌝ ∗
-                 Q z n ε (λ x, ε2 [x])
+                 _
             )%I with "[//][-]") as "?"; try done.
   Admitted.
   (*   { iMod "Hvs" as "(%ε & %ε2 & Herr &Hfrag & %Hpos & %Hineq & Hrest)". *)