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

State before:
α : Type
⊢ (s : Type) → (P : dLang α) → ν' (s · P) ≡ (s × ν' P)
Tactic:
intro P Q
State after:
α P : Type
Q : dLang α
⊢ ν' (P · Q) ≡ (P × ν' Q)

State before:
α P : Type
Q : dLang α
⊢ ν' (P · Q) ≡ (P × ν' Q)
Tactic:
constructor
State after:
case a
α P : Type
Q : dLang α
⊢ ν' (P · Q) = (P × ν' Q)

State before:
case a
α P : Type
Q : dLang α
⊢ ν' (P · Q) = (P × ν' Q)
Tactic:
rfl
State after:
no goals