This way, iSplit will work when one side is persistent.

This could lead to awkward loops, for example, when having:

- As goal `own γ c` with `c` persistent, one could keep on
  `iSplit`ting the goal. Especially in (semi-)automated proof
  scripts this is annoying as it easily leads to loops.
- When having a hypothesis `own γ c` with `c` persistent, one
  could keep on `iDestruct`ing it.

To that end, this commit removes the `IntoOp` and `FromOp` instances
for persistent CMRA elements. Instead, we changed the instances for
pairs, so that one, for example, can still split `(a ⋅ b, c)` with
`c` persistent.

This are useful as proofmode cannot always guess in which direction
it should use ⊣⊢.

This fixes issue #81.

Updating the ProofMode.md docs

See merge request !53

The instances frame_big_sepL_cons and frame_big_sepL_app could be
applied repeatedly often when framing in [∗ list] k ↦ x ∈ ?e, Φ k x
when ?e an evar. This commit fixes this bug.

- Allow framing of persistent hypotheses below the always modality.
- Allow framing of persistent hypotheses in just one branch of a
  disjunction.

This has some advantages:

- Evaluation contexts behave like a proper "Huet's zipper", and thus:
  + We no longer need to reverse the list of evaluation context items in the
    `reshape_expr` tactic.
  + The `fill` function becomes tail-recursive.
- It gives rise to more definitional equalities in simulation proofs using
  binary logical relations proofs.

  In the case of binary logical relations, we simulate an expressions in some
  ambient context, i.e. `fill K e`. Now, whenever we reshape `e` by turning it
  into `fill K' e'`, we end up with `fill K (fill K' e')`. In order to use the
  rules for the expression that is being simulated, we need to turn
  `fill K (fill K' e')` into `fill K'' e'` for some `K'`. In case of the old
  `foldr`-based approach, we had to rewrite using the lemma `fill_app` to
  achieve that. However, in case of the old `foldl`-based `fill`, we have that
  `fill K (fill K' e')` is definitionally equal to `fill (K' ++ K) e'` provided
  that `K'` consists of a bunch of `cons`es (which is always the case, since we
  obtained `K'` by reshaping `e`).

Note that this change hardly affected `heap_lang`. Only the proof of
`atomic_correct` broke. I fixed this by proving a more general lemma
`ectxi_language_atomic` about `ectxi`-languages, which should have been there
in the first place.