case refl
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝ b c d a : α
P : (a_1 : α) → ReflTransGen r a_1 a → Prop
refl : P a (_ : ReflTransGen r a a)
head : ∀ {a_1 c : α} (h' : r a_1 c) (h : ReflTransGen r c a), P c h → P a_1 (_ : ReflTransGen r a_1 a)
⊢ P a (_ : ReflTransGen r a a)

case tail
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝² b c d a b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ :
  ∀ {P : (a : α) → ReflTransGen r a b✝ → Prop},
    P b✝ (_ : ReflTransGen r b✝ b✝) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b✝), P c h → P a (_ : ReflTransGen r a b✝)) → P a a✝¹
P : (a : α) → ReflTransGen r a c✝ → Prop
refl : P c✝ (_ : ReflTransGen r c✝ c✝)
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c c✝), P c h → P a (_ : ReflTransGen r a c✝)
⊢ P a (_ : ReflTransGen r a c✝)
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝ b c d : α
P : (a : α) → ReflTransGen r a b → Prop
a : α
h : ReflTransGen r a b
refl : P b (_ : ReflTransGen r b b)
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)
⊢ P a h
induction h
case tail
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝² b c d a b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ :
  ∀ {P : (a : α) → ReflTransGen r a b✝ → Prop},
    P b✝ (_ : ReflTransGen r b✝ b✝) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b✝), P c h → P a (_ : ReflTransGen r a b✝)) → P a a✝¹
P : (a : α) → ReflTransGen r a c✝ → Prop
refl : P c✝ (_ : ReflTransGen r c✝ c✝)
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c c✝), P c h → P a (_ : ReflTransGen r a c✝)
⊢ P a (_ : ReflTransGen r a c✝)
case refl
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝ b c d a : α
P : (a_1 : α) → ReflTransGen r a_1 a → Prop
refl : P a (_ : ReflTransGen r a a)
head : ∀ {a_1 c : α} (h' : r a_1 c) (h : ReflTransGen r c a), P c h → P a_1 (_ : ReflTransGen r a_1 a)
⊢ P a (_ : ReflTransGen r a a)

case tail
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝² b c d a b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ :
  ∀ {P : (a : α) → ReflTransGen r a b✝ → Prop},
    P b✝ (_ : ReflTransGen r b✝ b✝) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b✝), P c h → P a (_ : ReflTransGen r a b✝)) → P a a✝¹
P : (a : α) → ReflTransGen r a c✝ → Prop
refl : P c✝ (_ : ReflTransGen r c✝ c✝)
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c c✝), P c h → P a (_ : ReflTransGen r a c✝)
⊢ P a (_ : ReflTransGen r a c✝)
case refl => exact refl
no goals
case tail
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝² b c d a b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ :
  ∀ {P : (a : α) → ReflTransGen r a b✝ → Prop},
    P b✝ (_ : ReflTransGen r b✝ b✝) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b✝), P c h → P a (_ : ReflTransGen r a b✝)) → P a a✝¹
P : (a : α) → ReflTransGen r a c✝ → Prop
refl : P c✝ (_ : ReflTransGen r c✝ c✝)
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c c✝), P c h → P a (_ : ReflTransGen r a c✝)
⊢ P a (_ : ReflTransGen r a c✝)
case tail b c _ hbc ih =>
refine @ih (λ {a : α} (hab : ReflTransGen r a b) => P a (ReflTransGen.tail hab hbc)) ?_ ?_
{ exact head hbc _ refl }
{ exact fun h1 h2 ↦ head h1 (h2.tail hbc) }
no goals
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝ b c d a : α
P : (a_1 : α) → ReflTransGen r a_1 a → Prop
refl : P a (_ : ReflTransGen r a a)
head : ∀ {a_1 c : α} (h' : r a_1 c) (h : ReflTransGen r c a), P c h → P a_1 (_ : ReflTransGen r a_1 a)
⊢ P a (_ : ReflTransGen r a a)
exact refl
case refine_1
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ (fun {a} hab => P a (_ : ReflTransGen r a c)) (_ : ReflTransGen r b b)

case refine_2
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b),
    (fun {a} hab => P a (_ : ReflTransGen r a c)) h →
      (fun {a} hab => P a (_ : ReflTransGen r a c)) (_ : ReflTransGen r a b)
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ P a (_ : ReflTransGen r a c)
refine @ih (λ {a : α} (hab : ReflTransGen r a b) => P a (ReflTransGen.tail hab hbc)) ?_ ?_
case refine_2
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b),
    (fun {a} hab => P a (_ : ReflTransGen r a c)) h →
      (fun {a} hab => P a (_ : ReflTransGen r a c)) (_ : ReflTransGen r a b)
case refine_1
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ (fun {a} hab => P a (_ : ReflTransGen r a c)) (_ : ReflTransGen r b b)

case refine_2
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b),
    (fun {a} hab => P a (_ : ReflTransGen r a c)) h →
      (fun {a} hab => P a (_ : ReflTransGen r a c)) (_ : ReflTransGen r a b)
{ exact head hbc _ refl }
no goals
case refine_2
α : Type u_1
β : Type ?u.16998
γ : Type ?u.17001
δ : Type ?u.17004
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b),
    (fun {a} hab => P a (_ : ReflTransGen r a c)) h →
      (fun {a} hab => P a (_ : ReflTransGen r a c)) (_ : ReflTransGen r a b)
{ exact fun h1 h2 ↦ head h1 (h2.tail hbc) }