{X : Type u_1} →
  [inst : NormedAddCommGroup X] →
    {M : Type u_2} →
      [inst_1 : Ring M] →
        [inst_2 : Module M X] →
          {P : M} →
            {motive : IsLprojection X P → Sort u} →
              ((proj : IsIdempotentElem P) → (Lnorm : ∀ (x : X), ‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖) → motive ⋯) →
                (t : IsLprojection X P) → motive t