[Agda] more about insertion to a list

[Sergei Meshveliani]

On Sat, 2017-02-18 at 21:21 +0300, Sergei Meshveliani wrote:
> Who can tell, please,
> why the attached code (about 30 nonempty lines) is not type-checked
> in Agda 2.6.0-e384ae7
> ?
> 
> Namely,  PE.refl  is reported in the end as having a wrong type.
> 
> The code is about the lemma  comm  below:
> 
> ----------------------------
> Mon = ℕ × ℕ
> 
> add : Mon → List Mon → List Mon
> add (a , e) []                 =  (a , e) ∷ []
> add (a , e) ((b , e') ∷ mons)  with compare e e'
> ...
>     | tri> _ _ _ = (a , e ) ∷ (b , e') ∷ mons
> ... | tri< _ _ _ = (b , e') ∷ (add (a , e) mons)
> ... | tri≈ _ _ _ = (a + b , e) ∷ mons
> 
> comm :  ∀ a e b e' mons → add (a , e ) (add (b , e') mons) ≡
>                           add (b , e') (add (a , e ) mons)
> ----------------------------
> 
> [..]

> Am I missing something? May be I misuse `inspect' and `rewrite' ?
> Can anybody fix the proof?


I manage with completing a proof only by inserting several constructs
of the kind  
            with compare x y | PE.inspect (compare x) y

These constructs are parasitic, because they are applied higher in the
code, and must work automatically in normalization. 

I wonder what is this effect with `inspect'. 

Regards,

------
Sergei