someLemma3 : {A : Set} {P : A → Set} {Q : A → Set} {B : Set} (f' : (∃ f ∈ (B → A) , (((b : B) → P (f b)) ∧ ((a : A) → P a → ((∃ b ∈ B , (f b == a))))))) → (((a : A) → P a → Q a) ↔ ((b : B) → Q ((π₁ f') b)))
  someLemma3 {A} {P} {Q} {B} (f , (hyp-a , hyp-b)) = (proof-a , proof-b)
   where
    proof-a :  ((a : A) → P a → Q a) → (b : B) → Q (f b)
    proof-a subhyp b = subhyp (f b) (hyp-a b)

    proof-b :  ((b : B) → Q (f b)) → (a : A) → P a → Q a
    proof-b subhyp a Pa = ([A==B]→A→B ([x==y]→[fx==fy] Q {f (π₁ (hyp-b a Pa))} {a} (π₂ (hyp-b a Pa)))) (subhyp (π₁ (hyp-b a Pa)))