wip: partial fixes for Parser.lean type errors

Changes across multiple files to address Lean 4 type system issues:

AST.lean:
- Add ToString instance for NormalForm (1NF, 2NF, 3NF, BCNF, 4NF)

IR.lean:
- Add ToString instance for ValidationLevel
- Add DecompositionStrategy type for normalization
- Simplify IR.Select to use Unit instead of polymorphic type
- Rename 'from' field to 'from_' (Lean keyword conflict)
- Fix CBOR serialization calls (use Serialization.encodeCBOR)
- Fix serializeProof to use CBOR simple value 21 for true

Parser.lean:
- Comment out parseToIR function (type inference failures)
- Replace with axiom stub for now
- Comment out example functions (unknown identifier 'Statement' errors)

Status: Parser module still has 15+ type errors that need deeper fixes.
The core parser combinators have type mismatches with Lean 4 expectations.
Lexer, TypeInference, and core IR modules continue to work correctly.

Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>

Author: Jonathan D.A. Jewell

src/FbqlDt/AST.lean

@@ -99,6 +99,15 @@ inductive NormalForm where
   | nf4 : NormalForm
   deriving Repr
 
+-- ToString for NormalForm
+instance : ToString NormalForm where
+  toString
+    | .nf1 => "1NF"
+    | .nf2 => "2NF"
+    | .nf3 => "3NF"
+    | .bcnf => "BCNF"
+    | .nf4 => "4NF"
+
 -- Type-safe values indexed by their types
 -- DEPENDS ON: TypeExpr
 inductive TypedValue : TypeExpr → Type where