constructor
case cons
α : Type u_1
R 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)
case cons.a
α : Type u_1
R 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
R 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