∀ n m p, O < p ⇒ ∀ x134 x135 x136, (x134 + (x135 + x136)) = (x135 + (x134 + x136))

Theorem let_clause_73 : forall (n:nat.nat), forall (m:nat.nat), forall (p:nat.nat), (nat.lt nat.O p) -> forall (x134:nat.nat), forall (x135:nat.nat), forall (x136:nat.nat), logic.eq (nat.nat) (nat.plus x134 (nat.plus x135 x136)) (nat.plus x135 (nat.plus x134 x136)).

theorem let_clause_73 : \forall (n:nat). \forall (m:nat). \forall (p:nat). ((lt) (O) p) -> \forall (x134:nat). \forall (x135:nat). \forall (x136:nat). (eq) (nat) ((plus) x134 ((plus) x135 x136)) ((plus) x135 ((plus) x134 x136)).

theorem let_clause_73 : forall (n:nat.nat) , forall (m:nat.nat) , forall (p:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (p)) -> forall (x134:nat.nat) , forall (x135:nat.nat) , forall (x136:nat.nat) , (((logic.eq_) (nat.nat)) ((((nat.plus) ) (x134)) ((((nat.plus) ) (x135)) (x136)))) ((((nat.plus) ) (x135)) ((((nat.plus) ) (x134)) (x136))).

let_clause_73 : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(p:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(p) => (FORALL(x134:nat_sttfa_th.sttfa_nat):(FORALL(x135:nat_sttfa_th.sttfa_nat):(FORALL(x136:nat_sttfa_th.sttfa_nat):logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.plus(x134)(nat_sttfa_th.plus(x135)(x136)))(nat_sttfa_th.plus(x135)(nat_sttfa_th.plus(x134)(x136))))))))))

Printing for OpenTheory is not working at the moment.