∀ m n, O < n ⇒ O = m ⇒ ∀ x1106, x1106 = (x1106 - m)

Theorem let_clause_1549 : forall (m:nat.nat), forall (n:nat.nat), (nat.lt nat.O n) -> (logic.eq (nat.nat) nat.O m) -> forall (x1106:nat.nat), logic.eq (nat.nat) x1106 (nat.minus x1106 m).

theorem let_clause_1549 : \forall (m:nat). \forall (n:nat). ((lt) (O) n) -> ((eq) (nat) (O) m) -> \forall (x1106:nat). (eq) (nat) x1106 ((minus) x1106 m).

theorem let_clause_1549 : forall (m:nat.nat) , forall (n:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (n)) -> ((((logic.eq_) (nat.nat)) ((nat.O) )) (m)) -> forall (x1106:nat.nat) , (((logic.eq_) (nat.nat)) (x1106)) ((((nat.minus) ) (x1106)) (m)).

let_clause_1549 : LEMMA (FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(n) => (logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.sttfa_O)(m) => (FORALL(x1106:nat_sttfa_th.sttfa_nat):logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](x1106)(nat_sttfa_th.minus(x1106)(m)))))))

Printing for OpenTheory is not working at the moment.