Skip to content
  • Robbert Krebbers's avatar
    Stronger "generic proper" lemmas for `big_op{L,M,S,MS}`. · 1078c169
    Robbert Krebbers authored
    - Renamed them from `_forall` into `_gen_proper`, to avoid confusion
      with `big_sep{L,M,S,MS}_forall`, which are actually about `∀`.
    - For lists and maps there now two variants, `_gen_proper_2`, in case
      the maps or lists on both sides are different, and `_gen_proper`,
      in case the maps or lists on both sides are the same.
    1078c169