Howdy,
I am a Coq newbie studying the nahas_tutorial.v (and things like that) in the Coq Ide.
Progress is tough enough for me to ask whether there might be a non-beginner who is willing to take some time, say, via ZOOM (login to be provided), to accelerate my progress.
My goal is to prove theorems in yet-to-be-specified but relatively simple multi-sorted first-order theories-with-equality-per-sort.
Many thanks for your help.
Ellis D. Cooper