simp [IContainer.Map]
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
i : I
α β γ : I → Type u₁
f : (i : I) → β i → γ i
g : (i : I) → α i → β i
fst✝ : A (IQPF.C F) i
snd✝ : (y : B (IQPF.C F) i fst✝) → α (N (IQPF.C F) i fst✝ y)
⊢ Map (fun i => f i ∘ g i) { fst := fst✝, snd := snd✝ } = Map f (Map g { fst := fst✝, snd := snd✝ })
no goals