]> matita.cs.unibo.it Git - helm.git/search
elim_tac rewritten almost entirely. It is now based on refinement +