case h.h
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a b = (a = b)
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ (Forall₂ fun x x_1 => x = x_1) = Eq
funext a b
case h.h.a
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a b ↔ a = b
case h.h
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a b = (a = b)
apply propext
case h.h.a.mp
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a b → a = b

case h.h.a.mpr
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ a = b → Forall₂ (fun x x_1 => x = x_1) a b
case h.h.a
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a b ↔ a = b
constructor
case h.h.a.mp
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
h : Forall₂ (fun x x_1 => x = x_1) a b
⊢ a = b
case h.h.a.mp
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a b → a = b
intro h
case h.h.a.mp.nil
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ [] = []

case h.h.a.mp.cons
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
a✝² b✝ : α
l₁✝ l₂✝ : List α
a✝¹ : a✝² = b✝
a✝ : Forall₂ (fun x x_1 => x = x_1) l₁✝ l₂✝
a_ih✝ : l₁✝ = l₂✝
⊢ a✝² :: l₁✝ = b✝ :: l₂✝
case h.h.a.mp
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
h : Forall₂ (fun x x_1 => x = x_1) a b
⊢ a = b
induction h
no goals
case h.h.a.mp.cons
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
a✝² b✝ : α
l₁✝ l₂✝ : List α
a✝¹ : a✝² = b✝
a✝ : Forall₂ (fun x x_1 => x = x_1) l₁✝ l₂✝
a_ih✝ : l₁✝ = l₂✝
⊢ a✝² :: l₁✝ = b✝ :: l₂✝
simp only [*]
no goals
case h.h.a.mp.nil
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ [] = []
rfl
case h.h.a.mpr
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a a
case h.h.a.mpr
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ a = b → Forall₂ (fun x x_1 => x = x_1) a b
rintro rfl
no goals
case h.h.a.mpr
α : Type u_1
β : Type ?u.14305
γ : Type ?u.14308
δ : Type ?u.14311
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a a
exact forall₂_refl _