theorem explosion (h : False) (P : Prop) : P :=
  False.elim h


theorem no_self_membership (α : Type u) : ¬ (α = α → False) :=
  fun h => h rfl

structure FormalSystem where
  axioms    : Prop          
  consistent : axioms → True 

inductive Result where
  | RussellEnters    : Result   
  | EmptyUnstable : Result 

def zfc_dilemma (forbids_self : Bool) : Result :=
  match forbids_self with
  | true  => Result.EmptyUnstable
  | false => Result.RussellEnters


def CircularProp (P : Prop) : Prop := P → P

theorem every_prop_is_circular (P : Prop) : CircularProp P :=
  fun hp => hp


theorem zfc_contradiction
    (foundation : ∀ (S : Prop), ¬ (S ∧ ¬S))  
    (self_ref   : ∃ (S : Prop), S ∧ ¬S)      
    : False := by
  obtain ⟨S, hS, hnS⟩ := self_ref
  exact foundation S ⟨hS, hnS⟩

theorem everything_is_true
    (foundation : ∀ (S : Prop), ¬ (S ∧ ¬S))
    (self_ref   : ∃ (S : Prop), S ∧ ¬S)
    (P : Prop) : P := by
  exact False.elim (zfc_contradiction foundation self_ref)