IsIntuitionistic should be generalised outside the `PL` scope, once we have typeclasses to express that a type possesses an implication connective.

[github-actions]

/-- An inference system is intuitionistic if it derives ex falso quodlibet. TODO: this should be
generalised outside the `PL` scope, once we have typeclasses to express that a type possesses an
implication connective. -/
@[scoped grind]
class IsIntuitionistic (Atom : Type u) [Bot Atom] (S : Type*)
    [InferenceSystem S (Proposition Atom)] where
  /-- The principle of explosion (ex falso quolibet). -/
  efq (A : Proposition Atom) : S⇓(⊥ → A)