∀ {X : Type u_2} [inst : NormedAddCommGroup X] {M : Type u_1} [inst_1 : Ring M] [inst_2 : Module M X]
  [inst_3 : FaithfulSMul M X] (P Q : { P // IsLprojection X P }), ↑P = ↑(P ⊓ Q) → ↑Q = ↑(Q ⊓ P) → P = Q