case mk
α : Type u_1
β : Type ?u.59102
γ : Type ?u.59105
inst✝ : DecidableEq α
y : α × α
x₁ x₂ : α
⊢ relBool (x₁, x₂) y = true ↔ Rel α (x₁, x₂) y
α : Type u_1
β : Type ?u.59102
γ : Type ?u.59105
inst✝ : DecidableEq α
x y : α × α
⊢ relBool x y = true ↔ Rel α x y
cases' x with x₁ x₂
case mk.mk
α : Type u_1
β : Type ?u.59102
γ : Type ?u.59105
inst✝ : DecidableEq α
x₁ x₂ y₁ y₂ : α
⊢ relBool (x₁, x₂) (y₁, y₂) = true ↔ Rel α (x₁, x₂) (y₁, y₂)
case mk
α : Type u_1
β : Type ?u.59102
γ : Type ?u.59105
inst✝ : DecidableEq α
y : α × α
x₁ x₂ : α
⊢ relBool (x₁, x₂) y = true ↔ Rel α (x₁, x₂) y
cases' y with y₁ y₂
no goals
case mk.mk
α : Type u_1
β : Type ?u.59102
γ : Type ?u.59105
inst✝ : DecidableEq α
x₁ x₂ y₁ y₂ : α
⊢ relBool (x₁, x₂) (y₁, y₂) = true ↔ Rel α (x₁, x₂) (y₁, y₂)
aesop (rule_sets [Sym2]) (add norm unfold [relBool])