1This material is a port of HOL Light material made available in commit 2 3 https://github.com/jrh13/hol-light/commit/013324af7ff715346383fb963d323138 4 5and described in John Harrison's paper ���Formalizing Basic First Order 6Model Theory��� from TPHOLs 1998 (DOI: 10.1007/BFb0055135). 7