λn. λm. λp. (mod n p) = (mod m p)

Definition congruent : nat.nat -> nat.nat -> nat.nat -> Prop := fun (n:nat.nat) => fun (m:nat.nat) => fun (p:nat.nat) => logic.eq (nat.nat) (div_mod.mod n p) (div_mod.mod m p)

definition congruent : nat -> nat -> nat -> Prop := \lambda n : nat. \lambda m : nat. \lambda p : nat. (eq) (nat) ((mod) n p) ((mod) m p)

def congruent : (nat.nat) -> (nat.nat) -> (nat.nat) -> Prop := fun (n : nat.nat) , fun (m : nat.nat) , fun (p : nat.nat) , (((logic.eq_) (nat.nat)) ((((div_mod.mod) ) (n)) (p))) ((((div_mod.mod) ) (m)) (p))

congruent : [nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> bool]]] = (LAMBDA(n:nat_sttfa_th.sttfa_nat):(LAMBDA(m:nat_sttfa_th.sttfa_nat):(LAMBDA(p:nat_sttfa_th.sttfa_nat):logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](div_mod_sttfa_th.mod(n)(p))(div_mod_sttfa_th.mod(m)(p)))))

Printing for OpenTheory is not working at the moment.