∀ x y h, ((x + h) - (y + h)) = (x - y)

Theorem minus_plus_plus_l : forall (x:nat), forall (y:nat), forall (h:nat), logic.eq (nat) (minus (plus x h) (plus y h)) (minus x y).

theorem minus_plus_plus_l : \forall (x:nat). \forall (y:nat). \forall (h:nat). (eq) (nat) ((minus) ((plus) x h) ((plus) y h)) ((minus) x y).

theorem minus_plus_plus_l : forall (x:nat.nat) , forall (y:nat.nat) , forall (h:nat.nat) , (((logic.eq_) (nat.nat)) ((((nat.minus) ) ((((nat.plus) ) (x)) (h))) ((((nat.plus) ) (y)) (h)))) ((((nat.minus) ) (x)) (y)).

minus_plus_plus_l : LEMMA (FORALL(x:nat_sttfa.sttfa_nat):(FORALL(y:nat_sttfa.sttfa_nat):(FORALL(h:nat_sttfa.sttfa_nat):logic_sttfa_th.eq[nat_sttfa.sttfa_nat](nat_sttfa.minus(nat_sttfa.plus(x)(h))(nat_sttfa.plus(y)(h)))(nat_sttfa.minus(x)(y)))))

Printing for OpenTheory is not working at the moment.