simp only [construct, M.destruct_construct, inv, true_and]
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x y : R
⊢ M.destruct (construct (Functor.Pure x)) =
      { fst := A.Pure x, snd := fun e => PEmpty.casesOn (fun x => M (Container C R)) e } ∧
    M.destruct (construct (Functor.Pure x)) =
        { fst := A.Pure x, snd := fun e => PEmpty.casesOn (fun x => M (Container C R)) e } ∧
      ∀ (i : Container.B (Container C R) (A.Pure x)),
        eq ((fun e => PEmpty.casesOn (fun x => M (Container C R)) e) i)
          ((fun e => PEmpty.casesOn (fun x => M (Container C R)) e) i)
case h₀.Pure.refl
C : _root_.Container
R : Type u₁
x y : R
⊢ ∀ (i : Container.B (Container C R) (A.Pure x)),
    eq (PEmpty.rec (fun x => M (Container C R)) i) (PEmpty.rec (fun x => M (Container C R)) i)