have ⟨_, y⟩ := wf
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
⊢ ∀ (x : B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
left✝ : Idx C (Container.M.destruct m).fst = i
y :
  ∀ (x : B C (Container.M.destruct m).fst),
    ↑(pgfp (WellFormedF C)) ⊥ (Next C (Container.M.destruct m).fst x) (PSigma.snd (Container.M.destruct m) x)
⊢ ∀ (x : B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)