Supporting version 2?

[JasonGross]

leanprover/lean4export@c9f8373 gives a format that works with the current version of rocq-lean-import

The current version gives

2.0.0
1 #NS 0 nat
2 #NS 1 O
3 #NS 1 S
1 #US 0
0 #ES 1
#IND 1 0 0 1 0 0 0 1 1 2 2 3 
1 #EC 1 
#CTOR 2 1 1 0 0 0 
4 #NS 0 a

which results in failure on the first line