case mk
α : Type u
β : α → Type v
γ : Type u_1
s₂ : AList β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ liftOn₂ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ ⟦s₂⟧ f H =
    f { entries := entries✝, nodupKeys := nodupKeys✝ } s₂
α : Type u
β : α → Type v
γ : Type u_1
s₁ s₂ : AList β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
⊢ liftOn₂ ⟦s₁⟧ ⟦s₂⟧ f H = f s₁ s₂
cases s₁
case mk.mk
α : Type u
β : α → Type v
γ : Type u_1
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
entries✝¹ : List (Sigma β)
nodupKeys✝¹ : NodupKeys entries✝¹
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ liftOn₂ ⟦{ entries := entries✝¹, nodupKeys := nodupKeys✝¹ }⟧ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ f H =
    f { entries := entries✝¹, nodupKeys := nodupKeys✝¹ } { entries := entries✝, nodupKeys := nodupKeys✝ }
case mk
α : Type u
β : α → Type v
γ : Type u_1
s₂ : AList β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ liftOn₂ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ ⟦s₂⟧ f H =
    f { entries := entries✝, nodupKeys := nodupKeys✝ } s₂
cases s₂
no goals
case mk.mk
α : Type u
β : α → Type v
γ : Type u_1
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
entries✝¹ : List (Sigma β)
nodupKeys✝¹ : NodupKeys entries✝¹
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ liftOn₂ ⟦{ entries := entries✝¹, nodupKeys := nodupKeys✝¹ }⟧ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ f H =
    f { entries := entries✝¹, nodupKeys := nodupKeys✝¹ } { entries := entries✝, nodupKeys := nodupKeys✝ }
rfl