| S | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| SBool | Data.Type.Natural, Data.Type.Natural.Builtin |
| sCmpNat | Data.Type.Natural, Data.Type.Natural.Builtin |
| sCompare | Data.Type.Natural, Data.Type.Natural.Builtin |
| sDiv | Data.Type.Natural, Data.Type.Natural.Builtin |
| SEQ | Data.Type.Natural, Data.Type.Natural.Builtin |
| SFalse | Data.Type.Natural, Data.Type.Natural.Builtin |
| sFlipOrdering | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| SGT | Data.Type.Natural, Data.Type.Natural.Builtin |
| sLeqCong | Data.Type.Natural.Lemma.Order |
| sLeqCongL | Data.Type.Natural.Lemma.Order |
| sLeqCongR | Data.Type.Natural.Lemma.Order |
| sLog2 | Data.Type.Natural, Data.Type.Natural.Builtin |
| SLT | Data.Type.Natural, Data.Type.Natural.Builtin |
| sMax | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| sMin | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| sMod | Data.Type.Natural, Data.Type.Natural.Builtin |
| SNat | Data.Type.Natural, Data.Type.Natural.Builtin |
| sNat | Data.Type.Natural, Data.Type.Natural.Builtin |
| snat | Data.Type.Natural, Data.Type.Natural.Builtin |
| sNatP | Data.Type.Natural, Data.Type.Natural.Builtin |
| sNatToOrd | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| sNatToOrd' | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| SomeNat | |
| 1 (Data Constructor) | Data.Type.Natural, Data.Type.Natural.Builtin |
| 2 (Type/Class) | Data.Type.Natural, Data.Type.Natural.Builtin |
| someNatVal | Data.Type.Natural, Data.Type.Natural.Builtin |
| SomeSNat | |
| 1 (Type/Class) | Data.Type.Natural, Data.Type.Natural.Builtin |
| 2 (Data Constructor) | Data.Type.Natural, Data.Type.Natural.Builtin |
| sOne | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| SOrdering | Data.Type.Natural, Data.Type.Natural.Builtin |
| sPred | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| sPred' | Data.Type.Natural.Lemma.Arithmetic |
| sS | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| sSucc | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| STrue | Data.Type.Natural, Data.Type.Natural.Builtin |
| Succ | |
| 1 (Type/Class) | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| 2 (Data Constructor) | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| succAndPlusOneL | Data.Type.Natural.Lemma.Arithmetic |
| succAndPlusOneR | Data.Type.Natural.Lemma.Arithmetic |
| succCong | Data.Type.Natural.Lemma.Arithmetic |
| succDiffNat | Data.Type.Natural.Lemma.Order |
| succInj | Data.Type.Natural.Lemma.Arithmetic |
| succInj' | Data.Type.Natural.Lemma.Arithmetic |
| succLeqAbsurd | Data.Type.Natural.Lemma.Order |
| succLeqAbsurd' | Data.Type.Natural.Lemma.Order |
| SuccLeqSucc | Data.Type.Natural.Lemma.Order |
| succLeqToLT | Data.Type.Natural.Lemma.Order |
| succLeqZeroAbsurd | Data.Type.Natural.Lemma.Order |
| succLeqZeroAbsurd' | Data.Type.Natural.Lemma.Order |
| succLneqSucc | Data.Type.Natural.Lemma.Order |
| succNonCyclic | Data.Type.Natural.Lemma.Arithmetic |
| succOneCong | Data.Type.Natural.Lemma.Arithmetic |
| succPred | Data.Type.Natural.Lemma.Arithmetic |
| sZero | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |