case H.a
α : Sort u_1
p : α → Prop
h : optParam (∀ (a : α), p a ↔ p (↑(Equiv.refl α) a)) (_ : ∀ (a : α), p a ↔ p a)
x✝ : { a // p a }
⊢ ↑(↑(subtypeEquiv (Equiv.refl α) h) x✝) = ↑(↑(Equiv.refl { a // p a }) x✝)
α : Sort u_1
p : α → Prop
h : optParam (∀ (a : α), p a ↔ p (↑(Equiv.refl α) a)) (_ : ∀ (a : α), p a ↔ p a)
⊢ subtypeEquiv (Equiv.refl α) h = Equiv.refl { a // p a }
ext
no goals
case H.a
α : Sort u_1
p : α → Prop
h : optParam (∀ (a : α), p a ↔ p (↑(Equiv.refl α) a)) (_ : ∀ (a : α), p a ↔ p a)
x✝ : { a // p a }
⊢ ↑(↑(subtypeEquiv (Equiv.refl α) h) x✝) = ↑(↑(Equiv.refl { a // p a }) x✝)
rfl