[Agda] "xs ≡ [] → " question

[Sergei Meshveliani]

Thanks to people for explanations.

On Fri, 2016-02-05 at 09:03 +0100, Andreas Abel wrote:
> g : ps ≡ [] → f ps ≡ 1
> g p rewrite p = PE.refl
> 

Great! I never used `rewrite', have forgotten of it.


> On 05.02.2016 06:24, effectfully wrote:
> > Also
> >      g : ps ≡ [] → f ps ≡ 1
> >      g r with ps | r
> >      ... | []    | _ = PE.refl
> >      ... | _ ∷ _ | ()
> 
> You can do with one clause here if you match on r instead of ps after 
> the with.

I see now. Thank you.

------
Sergei