rw [Container.Map_spec, Container.Map_spec, Container.Map_spec, Container.Map_spec]
case a.a.mk.mk
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
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x b : Quot (congr F)),
        r x b →
          Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
            Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map (fun i => (f ∘ Quot.mk r ∘ Quot.mk (congr F)) i) { fst := nx, snd := kx }) =
    abs (Container.Map (fun i => (f ∘ Quot.mk r ∘ Quot.mk (congr F)) i) { fst := ny, snd := ky })
case a.a.mk.mk
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
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x b : Quot (congr F)),
        r x b →
          Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
            Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map f (Container.Map (Quot.mk r) (Container.Map (Quot.mk (congr F)) { fst := nx, snd := kx }))) =
    abs (Container.Map f (Container.Map (Quot.mk r) (Container.Map (Quot.mk (congr F)) { fst := ny, snd := ky })))