theory MyInduction+− imports Main+− begin+−