Theorem: nullable_emptySet (Katydid/Conal/Calculus.lean)

State before:
⊢ (α : Type) → ν' ∅ ≡ PEmpty.{1}
Tactic:
intro α
State after:
α : Type
⊢ ν' ∅ ≡ PEmpty.{1}

State before:
α : Type
⊢ ν' ∅ ≡ PEmpty.{1}
Tactic:
constructor
State after:
case a
α : Type
⊢ ν' ∅ = PEmpty.{1}

State before:
case a
α : Type
⊢ ν' ∅ = PEmpty.{1}
Tactic:
rfl
State after:
no goals