∀ a b c, (a × (b × c)) = ((a × b) × c)

Theorem assoc : forall (a:nat.nat), forall (b:nat.nat), forall (c:nat.nat), logic.eq (nat.nat) (nat.times a (nat.times b c)) (nat.times (nat.times a b) c).

theorem assoc : \forall (a:nat). \forall (b:nat). \forall (c:nat). (eq) (nat) ((times) a ((times) b c)) ((times) ((times) a b) c).

theorem assoc : forall (a:nat.nat) , forall (b:nat.nat) , forall (c:nat.nat) , (((logic.eq_) (nat.nat)) ((((nat.times) ) (a)) ((((nat.times) ) (b)) (c)))) ((((nat.times) ) ((((nat.times) ) (a)) (b))) (c)).

assoc : LEMMA (FORALL(a:nat_sttfa_th.sttfa_nat):(FORALL(b:nat_sttfa_th.sttfa_nat):(FORALL(c:nat_sttfa_th.sttfa_nat):logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.times(a)(nat_sttfa_th.times(b)(c)))(nat_sttfa_th.times(nat_sttfa_th.times(a)(b))(c)))))

Printing for OpenTheory is not working at the moment.