∀ n p, n ≡ n [p]

Theorem congruent_n_n : forall (n:nat.nat), forall (p:nat.nat), congruent n n p.

theorem congruent_n_n : \forall (n:nat). \forall (p:nat). (congruent) n n p.

theorem congruent_n_n : forall (n:nat.nat) , forall (p:nat.nat) , ((((cong.congruent) ) (n)) (n)) (p).

congruent_n_n : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(p:nat_sttfa_th.sttfa_nat):cong_sttfa.congruent(n)(n)(p)))

Printing for OpenTheory is not working at the moment.