Skip to content
GitLab
Explore
Sign in
Iris
Iris
Issues
#67
iAssert does not support destructing existentials
It seems like I cannot use something like:
iAssert (∃ a, P a) with "[]" as (a) "H".