Update README.md

README.md

@@ -152,7 +152,6 @@ print(response.choices[0].message.reasoning)
 _Example Content_:
 <details>
 <summary>Expand</summary
-```
 To define transaction rules as an inductive proposition in Lean, you can create an inductive type that captures the valid transitions between states. This approach is particularly useful for modeling state machines and proving properties about transitions, such as invariants.
 
 Here is an example of how to define an inductive proposition for valid transitions in a simple counter machine:
@@ -192,7 +191,6 @@ lemma reach_positive : ∀ n > 0, CounterTrans 0 n
 In this simpler model, `CounterTrans` is defined with a single constructor `valid`, which allows for any state to transition to the next state by incrementing by 1. The lemma `reach_positive` is straightforward to prove by induction, leveraging the simplicity of the transition rules.
 
 This approach ensures that the proof remains concise and effective, avoiding unnecessary complexity in the transition rules. By using inductive propositions, we can effectively reason about state transitions and prove properties about the system.
-```
 </details>
 
 **_Tool-Calling_**