nialogic: fixed breaking tests
nialogic: got low-level proofs working