∀ f n, injn f (n+1) ⇒ injn f n

Theorem injn_Sn_n : forall (f:(nat.nat -> nat.nat)), forall (n:nat.nat), (injn f (nat.S n)) -> injn f n.

theorem injn_Sn_n : \forall (f:nat -> nat). \forall (n:nat). ((injn) f ((S) n)) -> (injn) f n.

theorem injn_Sn_n : forall (f:(nat.nat) -> nat.nat) , forall (n:nat.nat) , ((((permutation.injn) ) (f)) (((nat.S) ) (n))) -> (((permutation.injn) ) (f)) (n).

injn_Sn_n : LEMMA (FORALL(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(n:nat_sttfa_th.sttfa_nat):(permutation_sttfa.injn(f)(nat_sttfa_th.sttfa_S(n)) => permutation_sttfa.injn(f)(n))))

Printing for OpenTheory is not working at the moment.