Skip to content
GitLab
Explore
Sign in
Simon Friis Vindum
Iris
Repository
iris
iris
bi
big_op.v
Find file
Blame
History
Permalink
Generalize lemma `big_sepL2_app_inv` and use that to prove `big_sepL2_snoc`.
· ee535aa2
Robbert Krebbers
authored
Jan 17, 2021
ee535aa2