{P : Sort u} →
  {toSnapshot : Lean.Language.Snapshot} →
    {metaSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf} →
      {result? : Option Lean.Language.Lean.HeaderProcessedState} →
        {toSnapshot' : Lean.Language.Snapshot} →
          {metaSnap' : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf} →
            {result?' : Option Lean.Language.Lean.HeaderProcessedState} →
              { toSnapshot := toSnapshot, metaSnap := metaSnap, result? := result? } =
                  { toSnapshot := toSnapshot', metaSnap := metaSnap', result? := result?' } →
                (toSnapshot = toSnapshot' → metaSnap = metaSnap' → result? = result?' → P) → P