case a
a b c d : Prop
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
q₂ : Quotient s₂
q₃ : Quotient s₃
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
a✝ : α
⊢ motive (Quotient.mk s₁ a✝) q₂ q₃
a b c d : Prop
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
q₁ : Quotient s₁
q₂ : Quotient s₂
q₃ : Quotient s₃
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
⊢ motive q₁ q₂ q₃
induction q₁ using Quotient.ind
case a.a
a b c d : Prop
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
q₃ : Quotient s₃
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
a✝¹ : α
a✝ : β
⊢ motive (Quotient.mk s₁ a✝¹) (Quotient.mk s₂ a✝) q₃
case a
a b c d : Prop
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
q₂ : Quotient s₂
q₃ : Quotient s₃
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
a✝ : α
⊢ motive (Quotient.mk s₁ a✝) q₂ q₃
induction q₂ using Quotient.ind
case a.a.a
a b c d : Prop
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
a✝² : α
a✝¹ : β
a✝ : φ
⊢ motive (Quotient.mk s₁ a✝²) (Quotient.mk s₂ a✝¹) (Quotient.mk s₃ a✝)
case a.a
a b c d : Prop
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
q₃ : Quotient s₃
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
a✝¹ : α
a✝ : β
⊢ motive (Quotient.mk s₁ a✝¹) (Quotient.mk s₂ a✝) q₃
induction q₃ using Quotient.ind
no goals
case a.a.a
a b c d : Prop
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
a✝² : α
a✝¹ : β
a✝ : φ
⊢ motive (Quotient.mk s₁ a✝²) (Quotient.mk s₂ a✝¹) (Quotient.mk s₃ a✝)
apply h