no goals
α : Type u_1
β : Type u_2
γ : Type ?u.132020
δ : Type ?u.132023
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
hr : BiUnique R
a : α
b : β
x✝ : R a b
⊢ (fun x x_1 => x ∈ x_1) a [] ↔ (fun x x_1 => x ∈ x_1) b []
simp only [not_mem_nil]
α : Type u_1
β : Type u_2
γ : Type ?u.132020
δ : Type ?u.132023
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ a = a' ∨ a ∈ as ↔ b = b' ∨ b ∈ bs
α : Type u_1
β : Type u_2
γ : Type ?u.132020
δ : Type ?u.132023
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ (fun x x_1 => x ∈ x_1) a (a' :: as) ↔ (fun x x_1 => x ∈ x_1) b (b' :: bs)
simp only [mem_cons]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.132020
δ : Type ?u.132023
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ a = a' ∨ a ∈ as ↔ b = b' ∨ b ∈ bs
exact rel_or (rel_eq hr h h₁) (rel_mem hr h h₂)