Generate projectors for recursive structs during Lean extraction

[R1kM]

As described in #178, recursive Rust structs are extracted to Lean inductives due to Lean not supporting recursion in structures.
However, to retrieve similar functionalities, it would be useful to always extract projectors in this specific case, which is already done for the Coq backend.

[sonmarcho]

This solution actually also works for this issue (the problem is the same: Lean doesn't natively support recursive structures): #176

Also, we will have to find a way of automatically reducing projections (e.g., (Pair.mk 0 1).fst ~~> 0). I'm not sure what the best way to do that is: we could generate simplification lemmas and mark them as @simp but I think simp has a special attribute for projections. See this: https://github.com/leanprover-community/lean/blob/cce7990ea86a78bdb383e38ed7f9b5ba93c60ce0/library/init/meta/simp_tactic.lean#L276