no goals
case nil
α : Type u_1
β : Type ?u.2069
R S✝ T : α → α → Prop
a : α
l✝ : List α
S : α → α → Prop
l : List α
H : ∀ {a b : α}, a ∈ [] → b ∈ [] → R a b → S a b
⊢ Pairwise S []
constructor
case cons.a
α : Type u_1
β : Type ?u.2069
R S✝ T : α → α → Prop
a✝¹ : α
l✝¹ : List α
S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ ∀ (a' : α), a' ∈ l → S a a'

case cons.a
α : Type u_1
β : Type ?u.2069
R S✝ T : α → α → Prop
a✝¹ : α
l✝¹ : List α
S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S l
case cons
α : Type u_1
β : Type ?u.2069
R S✝ T : α → α → Prop
a✝¹ : α
l✝¹ : List α
S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S (a :: l)
constructor
no goals
case cons.a
α : Type u_1
β : Type ?u.2069
R S✝ T : α → α → Prop
a✝¹ : α
l✝¹ : List α
S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ ∀ (a' : α), a' ∈ l → S a a'
exact BAll.imp_right (fun x h ↦ H (mem_cons_self _ _) (mem_cons_of_mem _ h)) r
no goals
case cons.a
α : Type u_1
β : Type ?u.2069
R S✝ T : α → α → Prop
a✝¹ : α
l✝¹ : List α
S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S l
exact ih fun {a b} m m' ↦ H (mem_cons_of_mem _ m) (mem_cons_of_mem _ m')