[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)
> ----------------------------
> 
> [..]


In the attached code, a typo
                             tri> e>e' _ _  
needs to be replaced with
                             tri> _    _ e>e'

But this does not make difference because the identifier  e>e'  is used
only as a comment.