// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Theorem

nat.injective_S

Statement

injective S

Main Dependencies
Theory
Coq-Jumb
Statement

Theorem injective_S : relations.injective (nat) (nat) S.


Matita-Jumb
Statement

theorem injective_S : (injective) (nat) (nat) (S) .


Lean-jumb
Statement

theorem injective_S : ((relations.injective) (nat.nat) (nat.nat)) ((nat.S) ).


PVS-jumb
Statement

injective_S : LEMMA relations_sttfa_th.injective[nat_sttfa.sttfa_nat,nat_sttfa.sttfa_nat](nat_sttfa.sttfa_S)


OpenTheory

Printing for OpenTheory is not working at the moment.