Talk more about case eliminiation in mmil.html
Talk more about case eliminiation in mmil.html

This is mostly to try to extract a pattern from the successful
intuitionization of mosubopt .

Also mention pm5.21nii which is somewhat along the same lines.

metamath/set.mm,metamath/set.mm,metamath/set.mm