case h.mk.mk
α : Type u_1
β : Type ?u.16100
γ : Type ?u.16103
x✝ : Sym2 α
x y : α
⊢ map id (Quot.mk Setoid.r (x, y)) = id (Quot.mk Setoid.r (x, y))
α : Type u_1
β : Type ?u.16100
γ : Type ?u.16103
⊢ map id = id
ext ⟨⟨x, y⟩⟩
no goals
case h.mk.mk
α : Type u_1
β : Type ?u.16100
γ : Type ?u.16103
x✝ : Sym2 α
x y : α
⊢ map id (Quot.mk Setoid.r (x, y)) = id (Quot.mk Setoid.r (x, y))
rfl