[Agda] "xs ≡ [] → " question

[Sergei Meshveliani]

On Fri, 2016-02-05 at 21:50 +0400, Sergei Meshveliani wrote:
> 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
> > >      ... | _ ∷ _ | ()


I another example I have  Null : List A → Set _,  
with its constructor  isNull,
and 
    g :  Null ps → f ps ≡ 1#

So, `rewrite' cannot apply. But the second approach does work: 

    g nullPs  with ftPairs | nullPs
    ...            | []    | _  =  PE.refl
    ...            | _ ∷ _ | ()	

Thanks,

------
Sergei