simp only [destruct, destruct.f] at h₂
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
h₂ : Quot.mk r <$> destruct (Quot.mk (congr F) x) = Quot.mk r <$> destruct (Quot.mk (congr F) y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct x) =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))