Quantifier-free induction for lists

Stefan Hetzl, Jannik Vierling

We investigate quantifier-free induction for Lisp-like lists constructed inductively from the empty list $nil$ and the operation $cons$, that adds an element to t…