. clear h₂
  intro i x y h₂
  simp only [precongr, map_quot]
  have h₂ := h₁ i _ _ h₂
  simp only [destruct, destruct.f] at h₂
  generalize IContainer.M.destruct x = x at *
  generalize IContainer.M.destruct y = y at *
  cases x with | mk nx kx =>
  cases y with | mk ny ky =>
  let f i : Quot (r i) → Quot (r' i) :=
    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 : ∀ i, f i ∘ Quot.mk (r _) ∘ Quot.mk (congr F _) = Quot.mk (r' _) := by intro i; rfl
  conv =>
    congr
    . rhs
      lhs
      intro i
      rw [←this]
      rfl
    . rhs
      lhs
      intro i
      rw [←this]
  rw [IContainer.Map_spec, IContainer.Map_spec, IContainer.Map_spec, IContainer.Map_spec]
  rw [inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, h₂]
case a.a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
x y : IContainer.M (C F) i
h₂ : r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
⊢ ∀ (i : I) (x y : IContainer.M (C F) i), r' i x y → ↑(precongr F) r' i x y

case a.a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
x y : IContainer.M (C F) i
h₂ : r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
⊢ r' i x y
case a.a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
x y : IContainer.M (C F) i
h₂ : r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
⊢ r' i x y