λn. λm. match_nat_type n (λp. mod_aux n n p) m

Definition mod : nat.nat -> nat.nat -> nat.nat := fun (n:nat.nat) => fun (m:nat.nat) => nat.match_nat_type (nat.nat) n (fun (p:nat.nat) => mod_aux n n p) m

definition mod : nat -> nat -> nat := \lambda n : nat. \lambda m : nat. (match_nat_type) (nat) n (\lambda p : nat. (mod_aux) n n p) m

noncomputable def mod : (nat.nat) -> (nat.nat) -> nat.nat := fun (n : nat.nat) , fun (m : nat.nat) , ((((nat.match_nat_type) (nat.nat)) (n)) (fun (p : nat.nat) , ((((div_mod.mod_aux) ) (n)) (n)) (p))) (m)

mod : [nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]] = (LAMBDA(n:nat_sttfa_th.sttfa_nat):(LAMBDA(m:nat_sttfa_th.sttfa_nat):nat_sttfa_th.match_nat_type[nat_sttfa_th.sttfa_nat](n)((LAMBDA(p:nat_sttfa_th.sttfa_nat):div_mod_sttfa.mod_aux(n)(n)(p)))(m)))

Printing for OpenTheory is not working at the moment.