Backporting strict implicits

Stream: mathlib4

[Mario Carneiro]

Lean 4 does not support "strict implicit" mode any more, that is, @@foo. There are only 40 hits for @@ in mathlib, so it seems like a reasonable backport candidate. It's also not particularly hard to support in the porting tool, so we can also not backport.

[Sebastian Ullrich]

Fwiw, I encountered exactly one type where strict implicit binders looked nicer while preparing our lab course, for which the following wrapper seemed adequate:

structure StrictImplicitProp (p : Prop) : Prop where
  fn : p

instance : CoeFun (StrictImplicitProp p) (fun _ => p) where
  coe := StrictImplicitProp.fn

abbrev Env.Adequate (ρ : Env) (σ : State) : Prop :=
  StrictImplicitProp <| ∀ {x v}, ρ x = some v → σ x = some v