Added proof that m |= phi implies th(simpl(phi)) leq th(m)
Merge branch 'master' of github.com:RichardEvans/EL