no goals
α : Type u_1
β : Type ?u.7583
γ : Type ?u.7586
δ : Type ?u.7589
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ Forall₂ Rₐ [] [] ↔ ∀ (x : α), x ∈ [] → Rₐ x x
simp
no goals
α : Type u_1
β : Type ?u.7583
γ : Type ?u.7586
δ : Type ?u.7589
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : α
l : List α
⊢ Forall₂ Rₐ (a :: l) (a :: l) ↔ ∀ (x : α), x ∈ a :: l → Rₐ x x
simp [@forall₂_same l]