[Agda] rewriting reveals extra arguments

[Aaron Stump]

Hello, Agda community.  I am working on a development where rewriting 
can reveal extra arguments.  A self-contained example is below (tested 
with Agda 2.5.4.1; sorry I have not had time to upgrade to 2.6.x yet).  
I am wondering if there is a way these extra arguments can be matched on 
the left-hand side of the equation, rather than needing to handle them 
with abstractions on the right-hand side (as happens in the myfun 
example).  Agda does an amazing job when definitional equality reveals 
extra arguments.  I'm just wondering if there is a trick for when 
rewriting reveals them. Thanks for any advice.
Best,
Aaron
------------------------------------
module rewrite-reveal where

-- boilerplate for ≡
import Agda.Primitive
open Agda.Primitive public
   using    (Level ; _⊔_ ; lsuc ; lzero)
data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
   refl : x ≡ x
infix 3 _≡_
{-# BUILTIN EQUALITY _≡_ #-}

-- booleans
data 𝔹 : Set where
  tt : 𝔹
  ff : 𝔹

_&&_ : 𝔹 → 𝔹 → 𝔹
tt && b = b
ff && b = ff

if_then_else_ : ∀ {ℓ} {A : Set ℓ} → 𝔹 → A → A → A
if tt then y else z = y
if ff then y else z = z

-- rewriting reveals extra arguments
myfun : ∀{b : 𝔹} → b && b ≡ tt → if b && b then (𝔹 → 𝔹 → 𝔹) else 𝔹
myfun p rewrite p = λ x y → x

-- similar but unification resolves
myfun-easier : ∀{b : 𝔹} → b ≡ tt → if b then (𝔹 → 𝔹 → 𝔹) else 𝔹
myfun-easier refl x y = x