no goals
α : Type u_1
β : Type ?u.20321
γ : Type ?u.20324
δ : Type ?u.20327
r : α → α → Prop
a✝ b✝ c d : α
P : {a b : α} → TransGen r a b → Prop
a b : α
h : TransGen r a b
base : ∀ {a b : α} (h : r a b), P (_ : TransGen r a b)
ih : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P (_ : TransGen r a c)
⊢ P h
induction h with
| single h => exact base h
| tail hab hbc h_ih => exact ih hab (single hbc) h_ih (base hbc)
no goals
case single
α : Type u_1
β : Type ?u.20321
γ : Type ?u.20324
δ : Type ?u.20327
r : α → α → Prop
a✝ b✝¹ c d : α
P : {a b : α} → TransGen r a b → Prop
a b : α
base : ∀ {a b : α} (h : r a b), P (_ : TransGen r a b)
ih : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P (_ : TransGen r a c)
b✝ : α
h : r a b✝
⊢ P (_ : TransGen r a b✝)
exact base h
no goals
case tail
α : Type u_1
β : Type ?u.20321
γ : Type ?u.20324
δ : Type ?u.20327
r : α → α → Prop
a✝ b✝¹ c d : α
P : {a b : α} → TransGen r a b → Prop
a b : α
base : ∀ {a b : α} (h : r a b), P (_ : TransGen r a b)
ih : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P (_ : TransGen r a c)
b✝ c✝ : α
hab : TransGen r a b✝
hbc : r b✝ c✝
h_ih : P hab
⊢ P (_ : TransGen r a c✝)
exact ih hab (single hbc) h_ih (base hbc)