redefine null_star

Author: awalterschulze

Katydid/Regex/Calculus.lean

@@ -83,20 +83,23 @@ def null_concat {α: Type} {P Q: Lang α}:
   case invFun =>
     exact fun ⟨x, y⟩ => ⟨[], [], x, y, rfl⟩
 
+def null_star' {α: Type} {P: Lang α}:
+  null (star P) := by
+  simp
+  exists []
+  apply And.intro
+  · exact All.nil
+  · intro l hl
+    cases hl
+
 def null_star {α: Type} {P: Lang α}:
   null (star P) <-> True := by
   refine Iff.intro ?toFun ?invFun
   case toFun =>
     exact (fun _ => True.intro)
   case invFun =>
     intro t
-    simp
-    exists []
-    apply And.intro
-    · exact All.nil
-    · intro l
-      intro l'
-      cases l'
+    exact null_star'
 
 def derive_emptyset {α: Type} {a: α}:
   (derive emptyset a) = emptyset :=