[Agda] Unification assumes injective postulates?

[Dan Licata]

On Nov14, Andreas Abel wrote:
> The basic question here is how we should understand
>
>   postulate foo : Nat -> Nat
>
> I see two basic interpretations here:
>
> 1. foo is a fixed, arbitrary unknown function.
> 2. foo is a fixed, specific unknown function.
>
> Interpretation 1, which seems to be the one taken by Agda, allows to reduce 
> foo x == foo y to x == y, since there are non-constant functions.  A 
> postulate behaves like a module parameter or a function parameter (free 
> variable).

I'd like to understand what's going on here better.  I think it would be
bad for postulates to be *propositionally* injective, because then
e.g. the following logical-framework-style definition would be wrong:

  postulate
    bool : Set
    true : bool
    false : bool
    if : {X : Set} -> bool -> X -> X -> X
    beta1 : forall {X} {e1 e2 : X} -> Id (if true e1 e2) e1
    beta2 : forall {X} {e1 e2 : X} -> Id (if false e1 e2) e2

  if-inj : forall {X} {e e'} {e1 e2 : X} -> 
           Id (if e e1 e2) (if e' e1 e2) -> Id e e'
  if-inj p = ?

  -- get a contradiction from showing that 
  -- if true true true = if false true true  
  wrong : Id true false
  wrong = if-inj {bool} {true} {false} {true} {true} 
  	  (IdM.trans beta1 (IdM.sym beta2))

But Agda doesn't let me prove if-inj (I'm a few versions back, so let me
know if this changed).

On the other hand, the intuition that 

  if two neutral terms with the same head are definitionally equal, 
  then they have the same spine

makes sense to me.  Is this the property that justifies the move you're
making above?

On the other other hand, I can imagine situations where that fails,
because e.g. you have eta for coproducts definitionally.  

So, what is it about definitional equality that justifies that move from
foo x == foo y to x == y, and how does Agda know not to apply the same
reasoning to propositional equality?

Thanks!
-Dan