case nil
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝¹ b : α
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁✝ : ∀ (a : α), a ∈ l → p a
a✝ : α
ha✝ : p a✝
hl₂✝ : Chain S (f a✝ ha✝) (pmap f l hl₁✝)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
hl₁ : ∀ (a : α), a ∈ [] → p a
a : α
ha : p a
hl₂ : Chain S (f a ha) (pmap f [] hl₁)
⊢ Chain R a []

case cons
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝¹ b : α
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁✝ : ∀ (a : α), a ∈ l → p a
a✝ : α
ha✝ : p a✝
hl₂✝ : Chain S (f a✝ ha✝) (pmap f l hl₁✝)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
lh : α
lt : List α
l_ih : ∀ (hl₁ : ∀ (a : α), a ∈ lt → p a) {a : α} (ha : p a), Chain S (f a ha) (pmap f lt hl₁) → Chain R a lt
hl₁ : ∀ (a : α), a ∈ lh :: lt → p a
a : α
ha : p a
hl₂ : Chain S (f a ha) (pmap f (lh :: lt) hl₁)
⊢ Chain R a (lh :: lt)
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b : α
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁ : ∀ (a : α), a ∈ l → p a
a : α
ha : p a
hl₂ : Chain S (f a ha) (pmap f l hl₁)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
⊢ Chain R a l
induction' l with lh lt l_ih generalizing a
no goals
case nil
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝¹ b : α
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁✝ : ∀ (a : α), a ∈ l → p a
a✝ : α
ha✝ : p a✝
hl₂✝ : Chain S (f a✝ ha✝) (pmap f l hl₁✝)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
hl₁ : ∀ (a : α), a ∈ [] → p a
a : α
ha : p a
hl₂ : Chain S (f a ha) (pmap f [] hl₁)
⊢ Chain R a []
simp
no goals
case cons
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝¹ b : α
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁✝ : ∀ (a : α), a ∈ l → p a
a✝ : α
ha✝ : p a✝
hl₂✝ : Chain S (f a✝ ha✝) (pmap f l hl₁✝)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
lh : α
lt : List α
l_ih : ∀ (hl₁ : ∀ (a : α), a ∈ lt → p a) {a : α} (ha : p a), Chain S (f a ha) (pmap f lt hl₁) → Chain R a lt
hl₁ : ∀ (a : α), a ∈ lh :: lt → p a
a : α
ha : p a
hl₂ : Chain S (f a ha) (pmap f (lh :: lt) hl₁)
⊢ Chain R a (lh :: lt)
simp [H _ _ _ _ (rel_of_chain_cons hl₂), l_ih _ _ (chain_of_chain_cons hl₂)]