mathview Tool to adapt math proof granularity display. Good test theorems mp2 lukshef-ax1 dfss2 in0 ssrin t1lucas t2lucas ssun1 t4lucas t5lucas