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

State before:
α : Type u_1
⊢ (P Q : dLang α) → ν' (P , Q) ≃ ν' Q × ν' P
Tactic:
sorry
State after:
no goals