LRAT proof reconstruction for HOLSat

[ordinarymath]

We should be using LRAT for proof reconstruction for HOLSat instead of a range of not updated sat solvers with their own proof format. Note that @tanyongkiam mentions that hol-light[1] already supports this so it could be ported over.

[1] https://github.com/jrh13/hol-light/blob/master/Cadical/cadical.ml