mathlib3

a3a166bc - chore(model_theory/encoding): Improve the encoding of terms (#13532)

chore(model_theory/encoding): Improve the encoding of terms (#13532) Makes it so that the encoding of terms no longer requires the assumption `inhabited (L.term A)`. Adjusts following lemmas to use the `encoding` API more directly.