equal (gcd_aux_body O) (λm. λn. m)

Axiom axiom_gcd_aux_body_O : connectives.equal (nat.nat -> nat.nat -> nat.nat) (gcd_aux_body nat.O) (fun (m:nat.nat) => fun (n:nat.nat) => m)

axiom axiom_gcd_aux_body_O : (equal) (nat -> nat -> nat) ((gcd_aux_body) (O) ) (\lambda m : nat. \lambda n : nat. m)

axiom axiom_gcd_aux_body_O : (((connectives.equal) ((nat.nat) -> (nat.nat) -> nat.nat)) (((gcd.gcd_aux_body) ) ((nat.O) ))) (fun (m : nat.nat) , fun (n : nat.nat) , m)

axiom_gcd_aux_body_O : AXIOM connectives_sttfa_th.equal[[nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]]](gcd_sttfa.gcd_aux_body(nat_sttfa_th.sttfa_O))((LAMBDA(m:nat_sttfa_th.sttfa_nat):(LAMBDA(n:nat_sttfa_th.sttfa_nat):m)))

Printing for OpenTheory is not working at the moment.