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

case cons
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝¹ b : α
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
a✝ : α
l : List α
hl₁✝ : Chain R a✝ l
ha✝ : p a✝
hl₂✝ : ∀ (a : α), a ∈ l → p a
lh : α
lt : List α
l_ih : ∀ {a : α}, Chain R a lt → ∀ (ha : p a) (hl₂ : ∀ (a : α), a ∈ lt → p a), Chain S (f a ha) (pmap f lt hl₂)
a : α
hl₁ : Chain R a (lh :: lt)
ha : p a
hl₂ : ∀ (a : α), a ∈ lh :: lt → p a
⊢ Chain S (f a ha) (pmap f (lh :: lt) hl₂)
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b : α
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
a : α
l : List α
hl₁ : Chain R a l
ha : p a
hl₂ : ∀ (a : α), a ∈ l → p a
⊢ Chain S (f a ha) (pmap f l hl₂)
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 → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
a✝ : α
l : List α
hl₁✝ : Chain R a✝ l
ha✝ : p a✝
hl₂✝ : ∀ (a : α), a ∈ l → p a
a : α
hl₁ : Chain R a []
ha : p a
hl₂ : ∀ (a : α), a ∈ [] → p a
⊢ Chain S (f a ha) (pmap f [] hl₂)
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 → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
a✝ : α
l : List α
hl₁✝ : Chain R a✝ l
ha✝ : p a✝
hl₂✝ : ∀ (a : α), a ∈ l → p a
lh : α
lt : List α
l_ih : ∀ {a : α}, Chain R a lt → ∀ (ha : p a) (hl₂ : ∀ (a : α), a ∈ lt → p a), Chain S (f a ha) (pmap f lt hl₂)
a : α
hl₁ : Chain R a (lh :: lt)
ha : p a
hl₂ : ∀ (a : α), a ∈ lh :: lt → p a
⊢ Chain S (f a ha) (pmap f (lh :: lt) hl₂)
simp [H _ _ _ _ (rel_of_chain_cons hl₁), l_ih (chain_of_chain_cons hl₁)]