FL: add Finset alternative defs

Unused/FischerLadner.lean

@@ -1,4 +1,5 @@
 import Mathlib.Data.Finset.Basic
+import Mathlib.Data.Fintype.Basic
 import Mathlib.Order.FixedPoints
 
 import Pdl.Syntax
@@ -54,5 +55,30 @@ theorem le_flHom : X ≤ flHom X := by
 Note that we use `nextFixed` and not `lfp`. -/
 def fischerLadner (X : Set Formula) : Set Formula := OrderHom.nextFixed flHom X le_flHom
 
--- theorem fischerLadner_finite : (fischerLadner X).Finite := by
---   sorry
+theorem fischerLadner_finite : (fischerLadner X).Finite := by
+  sorry
+
+/-! ## Alternative approach with `Finset` -/
+
+def flStep_Finset : Finset Formula  → Finset Formula
+| X => X ∪ Finset.biUnion X flOf
+
+theorem flStep_Finset_isMonotone : Monotone flStep_Finset := by -- same proof
+  intro X Y h
+  simp_all only [Set.le_eq_subset, flStep_Finset]
+  intro x hx
+  simp at hx
+  cases hx <;> aesop
+
+def flHom_Finset : OrderHom (Finset Formula) (Finset Formula) := ⟨flStep_Finset, flStep_Finset_isMonotone⟩
+
+theorem le_flHom_Finset : X ≤ flHom_Finset X := by
+  intro f f_in
+  simp [flHom_Finset, flStep_Finset]
+  left
+  assumption
+
+def fischerLadner_Finset (X : Finset Formula) : Set Formula :=
+  -- OrderHom.nextFixed flHom_Finset X le_flHom
+  -- NOPE, because `Finset` is not a `CompleteLattice`
+  sorry