Skip to content
GitLab
Explore
Sign in
Iris
Iris
Repository
iris
theories
base_logic
lib
proph_map.v
Find file
Blame
History
Permalink
Add lemma `singleton_included : {[ i := x ]} ≼ ({[ i := y ]}
↔
x ≡ y ∨ x ≼ y`.
· 5ea9eab2
Robbert Krebbers
authored
Apr 03, 2020
Rename existing asymmetric lemma `singleton_included` into `singleton_included_l`.
5ea9eab2