generalize IContainer.M.destruct y = y at *
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✝
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
h₂✝ : r' i x✝ y
x : IContainer.Obj (C F) (IContainer.M (C F)) i
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i)) (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs x)) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs (IContainer.M.destruct y)))
⊢ abs (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)) x) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct 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✝
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
h₂✝ : r' i x✝ y✝
x y : IContainer.Obj (C F) (IContainer.M (C F)) i
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i)) (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs x)) =
    IFunctor.imap (fun i => Quot.mk (r i)) (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs y))
⊢ abs (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)) x) =
    abs (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)) y)