rf "Lid.ch". data Lnat -> N = Lzero: 1 -> N | Lsucc: Lid(N) -> N. def nat_2_Lnat: nat -> Lnat = n => {| zero: () => Lzero | succ: Ln => Lsucc (lid: Ln) |} n. def Lnat_2_nat: Lnat -> nat = Ln => {| Lzero: () => zero | Lsucc: n => succ lid n |} Ln. def Lone = () => Lsucc (lid: Lzero). def Ltwo = () => Lsucc (lid: Lone). def Lthree = () => Lsucc (lid: Ltwo). def Lfour = () => Lsucc (lid: Lthree). def Lfive = () => Lsucc (lid: Lfour). def Lsix = () => Lsucc (lid: Lfive). def Lseven = () => Lsucc (lid: Lsix). def Leight = () => Lsucc (lid: Lseven). def Lnine = () => Lsucc (lid: Leight). def Lten = () => Lsucc (lid: Lnine). def Lpred: Lnat -> Lnat = Lzero => Lzero | Lsucc n => lid n. def Ladd: Lnat * Lnat -> Lnat = (m, n) => {| Lzero: () => n | Lsucc: x => Lsucc x |} m. def Lmul: Lnat * Lnat -> Lnat = (m, n) => {| Lzero: () => Lzero | Lsucc: x => Ladd (n, lid x) |} m. def Lpow: Lnat * Lnat -> Lnat = (m, n) => {| Lzero: () => Lone | Lsucc: x => Lmul (m, lid x) |} n. def Lsub: Lnat * Lnat -> Lnat = (m, n) => {| Lzero: () => m | Lsucc: x => Lpred lid x |} n. def Lbig = () => Lpow (Lten, Lten).