leibniz (λm. λn. m) (mod_aux_body O)

Theorem sym_eq_mod_aux_body_O : leibniz.leibniz (nat.nat -> nat.nat -> nat.nat) (fun (m:nat.nat) => fun (n:nat.nat) => m) (mod_aux_body nat.O).

theorem sym_eq_mod_aux_body_O : (leibniz) (nat -> nat -> nat) (\lambda m : nat. \lambda n : nat. m) ((mod_aux_body) (O) ).

theorem sym_eq_mod_aux_body_O : (((leibniz.leibniz) ((nat.nat) -> (nat.nat) -> nat.nat)) (fun (m : nat.nat) , fun (n : nat.nat) , m)) (((div_mod.mod_aux_body) ) ((nat.O) )).

sym_eq_mod_aux_body_O : LEMMA leibniz_sttfa_th.leibniz[[nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]]]((LAMBDA(m:nat_sttfa_th.sttfa_nat):(LAMBDA(n:nat_sttfa_th.sttfa_nat):m)))(div_mod_sttfa.mod_aux_body(nat_sttfa_th.sttfa_O))

Printing for OpenTheory is not working at the moment.