no goals
α : Type u_3
β : Type u_2
γ : Type u_1
δ : Type ?u.456244
r : α → β → Prop
p : γ → δ → Prop
s : Multiset γ
f : γ → α
⊢ ∀ {t : Multiset β}, Rel r (map f 0) t ↔ Rel (fun a b => r (f a) b) 0 t
simp
no goals
α : Type u_3
β : Type u_2
γ : Type u_1
δ : Type ?u.456244
r : α → β → Prop
p : γ → δ → Prop
s : Multiset γ
f : γ → α
⊢ ∀ ⦃a : γ⦄ {s : Multiset γ},
    (∀ {t : Multiset β}, Rel r (map f s) t ↔ Rel (fun a b => r (f a) b) s t) →
      ∀ {t : Multiset β}, Rel r (map f (a ::ₘ s)) t ↔ Rel (fun a b => r (f a) b) (a ::ₘ s) t
simp (config := { contextual := true }) [rel_cons_left]