∀ n, n = (n × 1 )

Theorem times_n_1 : forall (n:nat), logic.eq (nat) n (times n (S O)).

theorem times_n_1 : \forall (n:nat). (eq) (nat) n ((times) n ((S) (O) )).

theorem times_n_1 : forall (n:nat.nat) , (((logic.eq_) (nat.nat)) (n)) ((((nat.times) ) (n)) (((nat.S) ) ((nat.O) ))).

times_n_1 : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):logic_sttfa_th.eq[nat_sttfa.sttfa_nat](n)(nat_sttfa.times(n)(nat_sttfa.sttfa_S(nat_sttfa.sttfa_O))))

Printing for OpenTheory is not working at the moment.