. apply reducible_iff.not.mpr;
  push_neg;
  obtain ⟨p, hp⟩ := noLEM (α := α);
  existsi (p ⋎ ~p);
  constructor;
  . exact lem!;
  . assumption;
case right
α : Type
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ≤ₛ 𝐈𝐧𝐭
no goals