mathlib

51adf3a1 - feat(model_theory/terms_and_formulas): Using a list encoding, bounds the number of terms (#12276)

feat(model_theory/terms_and_formulas): Using a list encoding, bounds the number of terms (#12276) Defines `term.list_encode` and `term.list_decode`, which turn terms into lists, and reads off lists as lists of terms. Bounds the number of terms by the number of allowed symbols + omega. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>