[Agda] proof for insertion to a list

[Sergei Meshveliani]

On Tue, 2017-02-14 at 19:50 +0100, G. Allais wrote:
> Hi Sergei,
> 
> Here's what I understand: `compare e e'` and `compare e' e`
> only show up in the goal's type *after* the values of `compare e e₁`
> and `compare e' e₁` have been uncovered and `add` has been able
> to reduce by one step.
> 
> So here you can't simply compute all the comparisons in parallel:
> you need cascading `with` blocks. The type of each one of these
> block being different from the previous thanks to the computations
> that happened.
> 
> I think that this is the sort of structure you're looking for:
> 
> ==========================================================
> add-comm (a , e) (b , e') ((c , e₁) ∷ mons)
>          with compare e e₁ | compare e' e₁
> 
> ... | tri> _ _ e>e₁ | tri> _ _ e'>e₁
>          with compare e e' | compare e' e
> 
> ... | tri> _ _ e>e' | tri< _ _ _  = {!!}
> 
> add-comm _ _  _ | _             | _           = anything
> ==========================================================
> 
> Now, in that new goal `compare e' e₁` shows up again. So you
> probably want to use inspect [1] to remember its value.
>
> [..]


Guillaume, thank you for help. 
I shall see. 

------
Sergei