a b c d : Prop
α : Sort u
β : α → Sort v
a₁ : α
b₁ b₂ : β a₁
h₂ : Eq.ndrec b₁ (_ : a₁ = a₁) = b₂
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := b₂ }
a b c d : Prop
α : Sort u
β : α → Sort v
a₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
h₁ : a₁ = a₂
h₂ : Eq.ndrec b₁ h₁ = b₂
⊢ { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
subst h₁
a b c d : Prop
α : Sort u
β : α → Sort v
a₁ : α
b₁ : β a₁
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := Eq.ndrec b₁ (_ : a₁ = a₁) }
a b c d : Prop
α : Sort u
β : α → Sort v
a₁ : α
b₁ b₂ : β a₁
h₂ : Eq.ndrec b₁ (_ : a₁ = a₁) = b₂
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := b₂ }
subst h₂
no goals
a b c d : Prop
α : Sort u
β : α → Sort v
a₁ : α
b₁ : β a₁
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := Eq.ndrec b₁ (_ : a₁ = a₁) }
exact rfl