[LRA proof] Recording & Printing LRA Proofs (#2758)

[LRA proof] Recording & Printing LRA Proofs (#2758)

* [LRA proof] Recording & Printing LRA Proofs

Now we use the ArithProofRecorder to record and later print arithmetic
proofs.

If an LRA lemma can be proven by a single farkas proof, then that is
done. Otherwise, we `trust` the lemma.

I haven't **really** enabled LRA proofs yet, so `--check-proofs` still
is a no-op for LRA.

To test, do
```
lfsccvc4 <(./bin/cvc4 --dump-proofs ../test/regress/regress0/lemmas/mode_cntrl.induction.smt | tail -n +2)
```

where `lfsccvc4` is an alias invoking `lfscc` with all the necessary
signatures. On my machine that is:

```
alias lfsccvc4="/home/aozdemir/repos/LFSC/build/src/lfscc \
/home/aozdemir/repos/CVC4/proofs/signatures/sat.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/smt.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/lrat.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_base.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_bv.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_bv_bitblast.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_arrays.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_int.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_quant.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf"

```

* Added guards to proof recording

Also reverted some small, unintentional changes.

Also had to add printing for STRING_SUBSTR??

* Responding to Yoni's review

* SimpleFarkasProof examples

* Respond to Aina's comments

* Reorder Constraint declarations

* fix build

* Moved friend declaration in Constraint

* Trichotomy example

* Lift getNumChildren invocation in PLUS case

Credits to aina for spotting it.

* Clang-format