1 回答
In fact it should be easy to show that get (ρ′ , x′) equals get (ε ∷ ρ′ , suc⁺ x′).
First, the reason that Agda does not see this equality is that the functions suc⁺ doesn't reduce for an argument of a general form x'. This is because your definition of suc⁺ pattern matches on the argument to see if it is a ε or a [_]. So, the simplest way to go further is to give Agda more information about the argument by pattern matching on x', so that suc⁺ x′ can reduce:
id≤get∘put {ρ = y ∷ ρ} [ suc x ] u
with put [ x ] u | id≤get∘put {ρ = ρ} [ x ] u
... | ρ′ , ε | u′ = u′
... | ρ′ , [ ._ ] | u′ = u′
With this extra pattern match, the type of u' reduces further to the expected type and everything works.
In your lemma not-ok, you have a very similar problem, that can be solved most easily by stating the lemma separately for x = ε or x = [_].
Working with heterogeneous equality is an option you might also explore to fix your problem, but I expect it will be more difficult than the options proposed here.