Allow DISPLAY to check whether a lambda is constant

[gallais]

As suggested by @mietek: it would be nice to be able to declare DISPLAY rules for the special case where a function is constant. For instance:

open import Agda.Builtin.Sigma
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

_×_ : (A B : Set) → Set
A × B = Σ A (λ _ → B)

∃ : {A : Set} (B : A → Set) → Set
∃ = Σ _

{-# DISPLAY Σ A (λ _ → B) = A × B #-}
{-# DISPLAY Σ A (λ x → B) = ∃ B   #-}

_ : Σ Nat (λ _ → Nat) -- shows up as Nat × Nat
_ = {!!}

_ : Σ Nat (λ n → 3 ≡ n) -- shows up as (∃ λ n → 3 ≡ n)
_ = {!!}