# add limit_preserving_impl'

This will help porting lambda-rust to Coq 8.16, where a proof using `limit_preserving_impl`

now fails.

Specifically this line. The first subgoal there is

`Proper (dist 0 ==> impl) (λ x : typeO, shr_locsE y3 (ty_size x + 1) ⊆ y2)`

which after a bunch of f_equiv becomes

`shr_locsE y3 (ty_size y6 + 1) ⊆ shr_locsE y3 (ty_size x + 1)`

and we don't have `Proper`

instances for `shr_locsE`

and `⊆`

.

On old Coq, something very strange happens when one does `f_equiv`

on that goal: it turns into

` (ty_size y6 + 1)%nat ⊆ (ty_size x + 1)%nat`

which, uh, shouldn't even typecheck? Without notation the term prints as

```
@subseteq nat (@eq nat) (Init.Nat.add (@ty_size Σ typeGS0 y6) 1)
(Init.Nat.add (@ty_size Σ typeGS0 x) 1)
```

So, this is actually `=@{nat}`

, but using `subseteq`

to print like `⊆`

... amazing. And also clearly nonsense. But this explains why the proof then used to complete: now we have an `=`

and `f_equiv`

continues to work fine.

In contrast, with the `_iff`

lemma, `f_equiv`

produces

` shr_locsE y3 (ty_size x + 1) ≡ shr_locsE y3 (ty_size y6 + 1)`

using the `≡`

on `gset`

. Another `f_equiv`

creates a goal with `≡@{nat}`

, using `ofe_equiv natO`

. With this, `solve_proper_core`

is able to complete the proof.