∀ f n, bijn f n ⇒ (f (n+1)) = (n+1) ⇒ bijn f (n+1)

Theorem bijn_n_Sn : forall (f:(nat.nat -> nat.nat)), forall (n:nat.nat), (bijn f n) -> (logic.eq (nat.nat) (f (nat.S n)) (nat.S n)) -> bijn f (nat.S n).

theorem bijn_n_Sn : \forall (f:nat -> nat). \forall (n:nat). ((bijn) f n) -> ((eq) (nat) (f ((S) n)) ((S) n)) -> (bijn) f ((S) n).

theorem bijn_n_Sn : forall (f:(nat.nat) -> nat.nat) , forall (n:nat.nat) , ((((permutation.bijn) ) (f)) (n)) -> ((((logic.eq_) (nat.nat)) ((f) (((nat.S) ) (n)))) (((nat.S) ) (n))) -> (((permutation.bijn) ) (f)) (((nat.S) ) (n)).

bijn_n_Sn : LEMMA (FORALL(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(n:nat_sttfa_th.sttfa_nat):(permutation_sttfa.bijn(f)(n) => (logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f(nat_sttfa_th.sttfa_S(n)))(nat_sttfa_th.sttfa_S(n)) => permutation_sttfa.bijn(f)(nat_sttfa_th.sttfa_S(n))))))

Printing for OpenTheory is not working at the moment.