. clear h₂
  intro x y h₂
  simp only [precongr, map_quot]
  have h₂ := h₁ _ _ h₂
  simp only [destruct, destruct.f] at h₂
  generalize Container.M.destruct x = x at *
  generalize Container.M.destruct y = y at *
  cases x with | mk nx kx =>
  cases y with | mk ny ky =>
  let f : Quot r → Quot r' :=
    by
      apply Quot.lift (Quot.lift (Quot.mk r') _) _
      . intro a b h₃
        apply Quot.sound
        simp only
        rw [Quot.sound h₃]
        apply h₀
      . intro x; apply Quot.inductionOn (motive := _) x; clear x
        intro x y; apply Quot.inductionOn (motive := _) y; clear y
        intro y h
        apply Quot.sound
        apply h
  have : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r' := rfl
  conv =>
    congr
    . rhs
      lhs
      intro i
      rw [←this]
      rfl
    . rhs
      lhs
      intro i
      rw [←this]
  rw [Container.Map_spec, Container.Map_spec, Container.Map_spec, Container.Map_spec]
  rw [inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, 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)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
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)), r' x y → ↑(precongr F) r' x 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)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x 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)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y