{P : Sort u} →
  {origCont : Lean.Elab.Do.DoElemCont} →
    {returnBase? breakBase? continueBase? : Option Lean.Elab.Do.ControlStack} →
      {pureBase : Lean.Elab.Do.ControlStack} →
        {pureDeadCode : Lean.Elab.Do.CodeLiveness} →
          {liftedDoBlockResultType : Lean.Expr} →
            {origCont' : Lean.Elab.Do.DoElemCont} →
              {returnBase?' breakBase?' continueBase?' : Option Lean.Elab.Do.ControlStack} →
                {pureBase' : Lean.Elab.Do.ControlStack} →
                  {pureDeadCode' : Lean.Elab.Do.CodeLiveness} →
                    {liftedDoBlockResultType' : Lean.Expr} →
                      { origCont := origCont, returnBase? := returnBase?, breakBase? := breakBase?,
                            continueBase? := continueBase?, pureBase := pureBase, pureDeadCode := pureDeadCode,
                            liftedDoBlockResultType := liftedDoBlockResultType } =
                          { origCont := origCont', returnBase? := returnBase?', breakBase? := breakBase?',
                            continueBase? := continueBase?', pureBase := pureBase', pureDeadCode := pureDeadCode',
                            liftedDoBlockResultType := liftedDoBlockResultType' } →
                        (origCont = origCont' →
                            returnBase? = returnBase?' →
                              breakBase? = breakBase?' →
                                continueBase? = continueBase?' →
                                  pureBase = pureBase' →
                                    pureDeadCode = pureDeadCode' →
                                      liftedDoBlockResultType = liftedDoBlockResultType' → P) →
                          P