Update README.md

README.md

@@ -1,7 +1,7 @@
-# Juvix Lean formalization library
+# Juvix library for Lean 4
 
 The Juvix Lean library provides primitives for verifying the correctness of Juvix compiler runs, i.e., proving that the semantics of a particular Juvix program is preserved by the compilation process.
 
-The major components of the library include:
-- formalization of Juvix compiler internal representations and their semantics,
-- proof-producing metaprograms for verifying that individual Juvix compiler transformations preserve the semantics.
+The library includes:
+- formalization of Juvix compiler internal representations (IRs) and their semantics,
+- proof-producing metaprograms for verifying that Juvix compiler transformations preserve the semantics of concrete IR programs.