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

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

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

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

let_clause_15491 : 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(x1106:nat_sttfa_th.sttfa_nat):logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](x1106)(nat_sttfa_th.minus(x1106)(n))))))

Printing for OpenTheory is not working at the moment.