Skip to content

Remove `map_Forall_insert_1_1` and `map_Forall_insert_1_2`

See discussion in !564 (comment 104221)

  • The names are not great
  • By using the ↔ lemma (i.e., map_Forall_insert one often gets simpler proofs, see iris@69446a0b for an example
  • At least Perennial still uses map_Forall_insert_1_1 and map_Forall_insert_1_2 so we should see if it's worth breaking backwards compatibility.