[GOAL]
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
h : ∀ (a : α), Subsingleton (motive (mk r a))
q : Quot r
f : (a : α) → motive (mk r a)
⊢ motive q
[PROOFSTEP]
induction q using Quot.rec
[GOAL]
case f
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
h : ∀ (a : α), Subsingleton (motive (mk r a))
f : (a : α) → motive (mk r a)
a✝ : α
⊢ motive (mk r a✝)
case h
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
h : ∀ (a : α), Subsingleton (motive (mk r a))
q : Quot r
f : (a : α) → motive (mk r a)
a✝ b✝ : α
p✝ : r a✝ b✝
⊢ (_ : mk r a✝ = mk r b✝) ▸ ?m.408 a✝ = ?m.408 b✝
[PROOFSTEP]
apply f
[GOAL]
case h
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
h : ∀ (a : α), Subsingleton (motive (mk r a))
q : Quot r
f : (a : α) → motive (mk r a)
a✝ b✝ : α
p✝ : r a✝ b✝
⊢ (_ : mk r a✝ = mk r b✝) ▸ f a✝ = f b✝
[PROOFSTEP]
apply Subsingleton.elim
