case nil
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
⊢ Pairwise R (map f []) ↔ Pairwise (fun a b => R (f a) (f b)) []

case cons
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : Pairwise R (map f tail✝) ↔ Pairwise (fun a b => R (f a) (f b)) tail✝
⊢ Pairwise R (map f (head✝ :: tail✝)) ↔ Pairwise (fun a b => R (f a) (f b)) (head✝ :: tail✝)
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
l : List α
⊢ Pairwise R (map f l) ↔ Pairwise (fun a b => R (f a) (f b)) l
induction l
case cons
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : Pairwise R (map f tail✝) ↔ Pairwise (fun a b => R (f a) (f b)) tail✝
⊢ Pairwise R (map f (head✝ :: tail✝)) ↔ Pairwise (fun a b => R (f a) (f b)) (head✝ :: tail✝)
case nil
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
⊢ Pairwise R (map f []) ↔ Pairwise (fun a b => R (f a) (f b)) []

case cons
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : Pairwise R (map f tail✝) ↔ Pairwise (fun a b => R (f a) (f b)) tail✝
⊢ Pairwise R (map f (head✝ :: tail✝)) ↔ Pairwise (fun a b => R (f a) (f b)) (head✝ :: tail✝)
. simp
no goals
case cons
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : Pairwise R (map f tail✝) ↔ Pairwise (fun a b => R (f a) (f b)) tail✝
⊢ Pairwise R (map f (head✝ :: tail✝)) ↔ Pairwise (fun a b => R (f a) (f b)) (head✝ :: tail✝)
. simp only [map, pairwise_cons, forall_mem_map_iff, *]
no goals
case nil
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
⊢ Pairwise R (map f []) ↔ Pairwise (fun a b => R (f a) (f b)) []
simp
no goals
case cons
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : Pairwise R (map f tail✝) ↔ Pairwise (fun a b => R (f a) (f b)) tail✝
⊢ Pairwise R (map f (head✝ :: tail✝)) ↔ Pairwise (fun a b => R (f a) (f b)) (head✝ :: tail✝)
simp only [map, pairwise_cons, forall_mem_map_iff, *]