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

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

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

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