α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.465503
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel (flip fun a b => flip r (f a) b) s t ↔ Rel (fun a b => r a (f b)) s t
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.465503
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel r s (map f t) ↔ Rel (fun a b => r a (f b)) s t
rw [← rel_flip, rel_map_left, ← rel_flip]
no goals
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.465503
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel (flip fun a b => flip r (f a) b) s t ↔ Rel (fun a b => r a (f b)) s t
rfl