Added fupd_plain_soundness_no_lc_strong

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