clear y
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 : IContainer.M (C F) i
y : M F i
⊢ ∀ (a : IContainer.M (C F) i),
    r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) a) → Quot.mk (congr F i) x = Quot.mk (congr F i) 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 : IContainer.M (C F) i
⊢ ∀ (a : IContainer.M (C F) i),
    r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) a) → Quot.mk (congr F i) x = Quot.mk (congr F i) a