{P : Sort u} →
  {lctx₁ : Lean.LocalContext} →
    {localInstances₁ : Lean.LocalInstances} →
      {lctx₂ : Lean.LocalContext} →
        {localInstances₂ : Lean.LocalInstances} →
          {equalFVarIds : Std.HashMap Lean.FVarId Lean.FVarId} →
            {lctx₁' : Lean.LocalContext} →
              {localInstances₁' : Lean.LocalInstances} →
                {lctx₂' : Lean.LocalContext} →
                  {localInstances₂' : Lean.LocalInstances} →
                    {equalFVarIds' : Std.HashMap Lean.FVarId Lean.FVarId} →
                      { lctx₁ := lctx₁, localInstances₁ := localInstances₁, lctx₂ := lctx₂,
                            localInstances₂ := localInstances₂, equalFVarIds := equalFVarIds } =
                          { lctx₁ := lctx₁', localInstances₁ := localInstances₁', lctx₂ := lctx₂',
                            localInstances₂ := localInstances₂', equalFVarIds := equalFVarIds' } →
                        (lctx₁ = lctx₁' →
                            localInstances₁ = localInstances₁' →
                              lctx₂ = lctx₂' → localInstances₂ = localInstances₂' → equalFVarIds = equalFVarIds' → P) →
                          P