From logically strongest to weakest we get:
If primitive equality is available in the signature and the comprehension, then leib(t,t') also implies t=t'. To get this take P to be lambda z. (t=z).
Note that the whole thing is actually far more complicated.
If you really want to get confused, have a look at the wonderful paper
"Higher Order Semantics and Extensionality" in
For example, we have implicitly assumed here that the type bool is non-trivial and satisfies tertium non datur, i.e. that our logic is two-valued. This implies that leib(_,_) is symmetric: From leib(t,t') we get (setting P to not Q), forall Q. (not Q(t) implies not Q(t')) and then its contrapositive forall Q. (not not Q(t') implies not not Q(t)). But in general only in classical logic we get forall Q. (Q(t') implies Q(t)), which means leib(t',t).