case h.h
α : Type uu
β : Type vv
l₁ l₂ : List α
γ : Type ?u.37152
δ : Type ?u.37155
r : α → β → Prop
p : γ → δ → Prop
a c : List α
⊢ (Perm ∘r Perm) a c = (a ~ c)
α : Type uu
β : Type vv
l₁ l₂ : List α
γ : Type ?u.37152
δ : Type ?u.37155
r : α → β → Prop
p : γ → δ → Prop
⊢ Perm ∘r Perm = Perm
funext a c
case h.h.a
α : Type uu
β : Type vv
l₁ l₂ : List α
γ : Type ?u.37152
δ : Type ?u.37155
r : α → β → Prop
p : γ → δ → Prop
a c : List α
⊢ (Perm ∘r Perm) a c ↔ a ~ c
case h.h
α : Type uu
β : Type vv
l₁ l₂ : List α
γ : Type ?u.37152
δ : Type ?u.37155
r : α → β → Prop
p : γ → δ → Prop
a c : List α
⊢ (Perm ∘r Perm) a c = (a ~ c)
apply propext
case h.h.a.mp
α : Type uu
β : Type vv
l₁ l₂ : List α
γ : Type ?u.37152
δ : Type ?u.37155
r : α → β → Prop
p : γ → δ → Prop
a c : List α
⊢ (Perm ∘r Perm) a c → a ~ c

case h.h.a.mpr
α : Type uu
β : Type vv
l₁ l₂ : List α
γ : Type ?u.37152
δ : Type ?u.37155
r : α → β → Prop
p : γ → δ → Prop
a c : List α
⊢ a ~ c → (Perm ∘r Perm) a c
case h.h.a
α : Type uu
β : Type vv
l₁ l₂ : List α
γ : Type ?u.37152
δ : Type ?u.37155
r : α → β → Prop
p : γ → δ → Prop
a c : List α
⊢ (Perm ∘r Perm) a c ↔ a ~ c
constructor
no goals
case h.h.a.mp
α : Type uu
β : Type vv
l₁ l₂ : List α
γ : Type ?u.37152
δ : Type ?u.37155
r : α → β → Prop
p : γ → δ → Prop
a c : List α
⊢ (Perm ∘r Perm) a c → a ~ c
exact fun ⟨b, hab, hba⟩ => Perm.trans hab hba
no goals
case h.h.a.mpr
α : Type uu
β : Type vv
l₁ l₂ : List α
γ : Type ?u.37152
δ : Type ?u.37155
r : α → β → Prop
p : γ → δ → Prop
a c : List α
⊢ a ~ c → (Perm ∘r Perm) a c
exact fun h => ⟨a, Perm.refl a, h⟩