Structural equality of Pi Types with heterogeneous equality?
I am not aware that J or K exists for heterogeneous equality. It does not need an elimination principle, because it can be simply defined as a sigma type:

coe : ∀{i}{A B : Set i} → A ≡ B → A → B

HEq : ∀ {i}{A B : Set i} → A → B → Set _
HEq {_}{A} {B} x y = Σ (A ≡ B) λ p → coe p x ≡ y


To do anything with HEq, it is enough to consider J and K for propositional equality. Dependent pattern matching is usually equivalent to J + K, although in Agda we can have pattern matching which is equivalent only to J.

So the question boils down to whether we can prove your lemma with J, or we need K as well. I prefer to work with uniqueness of identity proofs (UIP) instead of K (they are logically equivalent), so let's do that.

UIP : ∀ {i}{A : Set i}{x : A}{p : x ≡ x} → p ≡ refl


The answer is that we need UIP. Writing the lemma in Agda:

lem :
  ∀ (A₀ A₁ : Set)
    (A₀₁ : HEq A₀ A₁)
    (B₀ : A₀ → Set)
    (B₁ : A₁ → Set)
    (B₀₁ : HEq B₀ B₁)
  → HEq (∀ x → B₀ x) (∀ x → B₁ x)
lem A₀ A₁ (p , A₀₁) B₀ B₁ (q , B₀₁) = ?


It jumps at us that

A₀₁ : coe p A₀ ≡ A₁
p   : Set ≡ Set


In the absence of UIP, it is not provable that A₀ ≡ A₁, and therefore lem is not provable either. We can make it work with UIP. Agda code with intentionally puritan J usage:

{-# OPTIONS --without-K #-}

open import Data.Product

infix 4 _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

postulate
  UIP : ∀ {i}{A : Set i}{x : A}{p : x ≡ x} → p ≡ refl

J :
  ∀ {α β}{A : Set α} {x : A}(P : ∀ y → x ≡ y → Set β)
  → P x refl → {y : A} → (w : x ≡ y) → P y w
J P pr refl = pr

tr : ∀ {i j}{A : Set i}(B : A → Set j){a₀ : A}{a₁ : A}(a₂ : a₀ ≡ a₁) → B a₀ → B a₁
tr B p x = J (λ x _ → B x) x p

coe : ∀{i}{A B : Set i} → A ≡ B → A → B
coe = tr (λ x → x)

ap : ∀{i j}{A : Set i}{B : Set j}(f : A → B){a₀ a₁ : A}(a₂ : a₀ ≡ a₁)
     → f a₀ ≡ f a₁
ap f p = tr (λ a₁ → f _ ≡ f a₁) p refl

sym : ∀ {i}{A : Set i}{x y : A} → x ≡ y → y ≡ x
sym p = tr (λ y → y ≡ _) p refl

HEq : ∀ {i}{A B : Set i} → A → B → Set _
HEq {_}{A} {B} x y = Σ (A ≡ B) λ p → coe p x ≡ y

lem :
  ∀ (A₀ A₁ : Set)
    (A₀₁ : HEq A₀ A₁)
    (B₀ : A₀ → Set)
    (B₁ : A₁ → Set)
    (B₀₁ : HEq B₀ B₁)
  → HEq (∀ x → B₀ x) (∀ x → B₁ x)
lem A₀ A₁ (p , A₀₁) B₀ B₁ (q , B₀₁) =
  tr (λ p → (A₀₁ : coe p A₀ ≡ A₁) → HEq (∀ x → B₀ x) (∀ x → B₁ x))
     (sym (UIP {p = p}))
     (λ A₀₁ →
          refl ,
          J (λ A₁ A₀₁ → ∀ B₀ B₁ (q : (A₀ → Set) ≡ (A₁ → Set))
                      → coe q B₀ ≡ B₁
                      → ((x : A₀) → B₀ x) ≡ ((x : A₁) → B₁ x))
            (λ B₀ B₁ q B₀₁ →
               tr (λ q → coe q B₀ ≡ B₁ → ((x : A₀) → B₀ x) ≡ ((x : A₀) → B₁ x))
                  (sym (UIP {p = q}))
                  (λ B₀₁ → ap (λ f → ∀ x → f x) B₀₁)
                  B₀₁)
            A₀₁ B₀ B₁ q B₀₁)
     A₀₁


This might seem a handful, but after some practice such code is a mechanical exercise which generally follows the compilation of pattern matching. 

At this point we might ask if a variant of the lemma is provable only with J. The following is such, for example.

lemJ :
  ∀ (A₀ A₁ : Set)
    (A₀₁ : A₀ ≡ A₁)
    (B₀ : A₀ → Set)
    (B₁ : A₁ → Set)
    (B₀₁ : tr (λ X → X → Set) A₀₁ B₀ ≡ B₁)
  → (∀ x → B₀ x) ≡ (∀ x → B₁ x)
lemJ A₀ A₁ A₀₁ B₀ B₁ B₀₁ =
  J (λ A₁ A₀₁ → ∀ B₀ B₁ (B₀₁ : tr (λ X → X → Set) A₀₁ B₀ ≡ B₁)
              → ((x : A₀) → B₀ x) ≡ ((x : A₁) → B₁ x))
    (λ B₀ B₁ B₀₁ → ap (λ f → ∀ x → f x) B₀₁)
    A₀₁ B₀ B₁ B₀₁