Add tactic proof for nullable_char

katydid · Dec 10, 2023 · c8e9a86 · c8e9a86
1 parent 2af7110
commit c8e9a86
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/Katydid/Conal/Calculus.lean b/Katydid/Conal/Calculus.lean
@@ -60,8 +60,12 @@ theorem nullable_char:
   ∀ (c: α),
     ν (char c) <-> PEmpty := by
   intro α
-  -- TODO
-  sorry
+  simp
+  apply TIff.intro
+  intro
+  contradiction
+  intro
+  contradiction
 
 -- ν∪  : ν (P ∪ Q) ≡ (ν P ⊎ ν Q)
 -- ν∪ = refl