α : Type u_1
β : Type u_2
γ : Type ?u.442937
δ : Type ?u.442940
r : α → β → Prop
p : γ → δ → Prop
a : Multiset α
⊢ (a = 0 ∧ 0 = 0 ∨
      Exists fun {a_1} =>
        Exists fun {b} => Exists fun {as} => Exists fun {bs} => r a_1 b ∧ Rel r as bs ∧ a = a_1 ::ₘ as ∧ 0 = b ::ₘ bs) ↔
    a = 0
α : Type u_1
β : Type u_2
γ : Type ?u.442937
δ : Type ?u.442940
r : α → β → Prop
p : γ → δ → Prop
a : Multiset α
⊢ Rel r a 0 ↔ a = 0
rw [Rel_iff]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.442937
δ : Type ?u.442940
r : α → β → Prop
p : γ → δ → Prop
a : Multiset α
⊢ (a = 0 ∧ 0 = 0 ∨
      Exists fun {a_1} =>
        Exists fun {b} => Exists fun {as} => Exists fun {bs} => r a_1 b ∧ Rel r as bs ∧ a = a_1 ::ₘ as ∧ 0 = b ::ₘ bs) ↔
    a = 0
simp