fsdoc: no-summary-found
fsdoc: no-comment-found
* The modifies clause val loc_union_idem:s:loc -> (Lemma (==(loc_union s s, s)) (Prims.Cons (SMTPat (loc_union s s)) (Prims.Nil )))The following is useful to make Z3 cut matching loops with modifies_trans and modifies_refl
The modifies clause proper BEGIN TODO: move to FStar.Monotonic.HyperStack END TODO