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

State before:
α : Type (max u_1 u_2)
⊢ (P Q : dLang α) → ν' (P ⋃ Q) ≡ (ν' P ⊕ ν' Q)
Tactic:
intro P Q
State after:
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋃ Q) ≡ (ν' P ⊕ ν' Q)

State before:
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋃ Q) ≡ (ν' P ⊕ ν' Q)
Tactic:
constructor
State after:
case a
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋃ Q) = (ν' P ⊕ ν' Q)

State before:
case a
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋃ Q) = (ν' P ⊕ ν' Q)
Tactic:
rfl
State after:
no goals