α : Type u_1
β : Type u_2
γ : Type ?u.451251
δ : Type ?u.451254
r : α → β → Prop
p : γ → δ → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ (∃ bs₀_1 bs₁_1, Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔
    ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁
α : Type u_1
β : Type u_2
γ : Type ?u.451251
δ : Type ?u.451254
r : α → β → Prop
p : γ → δ → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ Rel r as (bs₀ + bs₁) ↔ ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁
rw [← rel_flip, rel_add_left]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.451251
δ : Type ?u.451254
r : α → β → Prop
p : γ → δ → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ (∃ bs₀_1 bs₁_1, Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔
    ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁
simp [rel_flip]