feat: flatten parent projections when pretty printing structure instance notation (#3749)

Given
```lean
structure A where
  x : Nat

structure B extends A where
  y : Nat
```
rather than pretty printing `{ x := 1, y := 2 : B }` as `{ toA := { x :=
1 }, y := 2 }`, it now pretty prints as `{ x := 1, y := 2 }`.

The option `pp.structureInstances.flatten` controls whether to flatten
structure instances like this.
9 files changed