proper transfer of theorems that involve classes being instantiated here;
(*<*)theory fakenat imports Main begin;(*>*)text{*\noindentThe type \tydx{nat} of naturalnumbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}. It behaves as if it were declared like this:*}datatype nat = 0 | Suc nat(*<*)end(*>*)