∀ m n, O = n ⇒ ∀ x347, n = (x347 × n)

Theorem let_clause_1551 : forall (m:nat.nat), forall (n:nat.nat), (logic.eq (nat.nat) nat.O n) -> forall (x347:nat.nat), logic.eq (nat.nat) n (nat.times x347 n).

theorem let_clause_1551 : \forall (m:nat). \forall (n:nat). ((eq) (nat) (O) n) -> \forall (x347:nat). (eq) (nat) n ((times) x347 n).

theorem let_clause_1551 : forall (m:nat.nat) , forall (n:nat.nat) , ((((logic.eq_) (nat.nat)) ((nat.O) )) (n)) -> forall (x347:nat.nat) , (((logic.eq_) (nat.nat)) (n)) ((((nat.times) ) (x347)) (n)).

let_clause_1551 : LEMMA (FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.sttfa_O)(n) => (FORALL(x347:nat_sttfa_th.sttfa_nat):logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](n)(nat_sttfa_th.times(x347)(n))))))

Printing for OpenTheory is not working at the moment.