∀ p, transitive (λn. λm. n ≡ m [p])

Theorem transitive_congruent : forall (p:nat.nat), relations.transitive (nat.nat) (fun (n:nat.nat) => fun (m:nat.nat) => congruent n m p).

theorem transitive_congruent : \forall (p:nat). (transitive) (nat) (\lambda n : nat. \lambda m : nat. (congruent) n m p).

theorem transitive_congruent : forall (p:nat.nat) , ((relations.transitive) (nat.nat)) (fun (n : nat.nat) , fun (m : nat.nat) , ((((cong.congruent) ) (n)) (m)) (p)).

transitive_congruent : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):relations_sttfa_th.transitive[nat_sttfa_th.sttfa_nat]((LAMBDA(n:nat_sttfa_th.sttfa_nat):(LAMBDA(m:nat_sttfa_th.sttfa_nat):cong_sttfa.congruent(n)(m)(p)))))

Printing for OpenTheory is not working at the moment.