no goals
α : Type uu
β : Type vv
l₁ l₂ : List α
γ : Type ?u.39471
δ : Type ?u.39474
r : α → β → Prop
p : γ → δ → Prop
hr : RightUnique r
a : List α
b : List β
h₁ : Forall₂ r a b
c : List α
d : List β
h₂ : Forall₂ r c d
h : a ~ c
this : (flip (Forall₂ r) ∘r Perm ∘r Forall₂ r) b d
⊢ ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d
rwa [← forall₂_comp_perm_eq_perm_comp_forall₂, ← Relation.comp_assoc] at this