requested to merge jihgfee/iris-coq:fupd_plain_soundness_no_lc_strong into master
Added the lemma
fupd_plain_soundness_no_lc_strong, which is a generalisation of the adequacy theorem of the Trillium instance of Iris.
Notably, it lifts the original soundness theorem to be a greatest fixpoint of nested fancy updates. The soundness theorem was primarily conducted by @amintimany .
EDIT: I was confused by the inclusion of
£ m in the
_no_lc lemmas, but added it here for consistency.
Since the proofs are strictly in the realm of
has_no_lc it seems superfluous to include them (even for future-proving)
EDIT 2: The theorem that this is used for can be found here https://github.com/logsem/aneris/blob/47375625241a7c03b98105984a27df8fc2e69ac9/trillium/program_logic/adequacy.v#L806