∀ a b q r q1 r1, div_mod_spec a b q r ⇒ div_mod_spec a b q1 r1 ⇒ r = r1

Theorem div_mod_spec_to_eq2 : forall (a:nat.nat), forall (b:nat.nat), forall (q:nat.nat), forall (r:nat.nat), forall (q1:nat.nat), forall (r1:nat.nat), (div_mod_spec a b q r) -> (div_mod_spec a b q1 r1) -> logic.eq (nat.nat) r r1.

theorem div_mod_spec_to_eq2 : \forall (a:nat). \forall (b:nat). \forall (q:nat). \forall (r:nat). \forall (q1:nat). \forall (r1:nat). ((div_mod_spec) a b q r) -> ((div_mod_spec) a b q1 r1) -> (eq) (nat) r r1.

theorem div_mod_spec_to_eq2 : forall (a:nat.nat) , forall (b:nat.nat) , forall (q:nat.nat) , forall (r:nat.nat) , forall (q1:nat.nat) , forall (r1:nat.nat) , ((((((div_mod.div_mod_spec) ) (a)) (b)) (q)) (r)) -> ((((((div_mod.div_mod_spec) ) (a)) (b)) (q1)) (r1)) -> (((logic.eq_) (nat.nat)) (r)) (r1).

div_mod_spec_to_eq2 : LEMMA (FORALL(a:nat_sttfa_th.sttfa_nat):(FORALL(b:nat_sttfa_th.sttfa_nat):(FORALL(q:nat_sttfa_th.sttfa_nat):(FORALL(r:nat_sttfa_th.sttfa_nat):(FORALL(q1:nat_sttfa_th.sttfa_nat):(FORALL(r1:nat_sttfa_th.sttfa_nat):(div_mod_sttfa.div_mod_spec(a)(b)(q)(r) => (div_mod_sttfa.div_mod_spec(a)(b)(q1)(r1) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](r)(r1)))))))))

Printing for OpenTheory is not working at the moment.