∀ R, ∀ n, R O n ⇒ ∀ n, R (n+1) O ⇒ ∀ n m, R n m ⇒ R (n+1) (m+1) ⇒ ∀ n m, R n m

Theorem nat_elim2 : forall (R:(nat -> nat -> Prop)), (forall (n:nat), R O n) -> (forall (n:nat), R (S n) O) -> (forall (n:nat), forall (m:nat), (R n m) -> R (S n) (S m)) -> forall (n:nat), forall (m:nat), R n m.

theorem nat_elim2 : \forall (R:nat -> nat -> Prop). (\forall (n:nat). R (O) n) -> (\forall (n:nat). R ((S) n) (O) ) -> (\forall (n:nat). \forall (m:nat). (R n m) -> R ((S) n) ((S) m)) -> \forall (n:nat). \forall (m:nat). R n m.

theorem nat_elim2 : forall (R:(nat.nat) -> (nat.nat) -> Prop) , (forall (n:nat.nat) , ((R) ((nat.O) )) (n)) -> (forall (n:nat.nat) , ((R) (((nat.S) ) (n))) ((nat.O) )) -> (forall (n:nat.nat) , forall (m:nat.nat) , (((R) (n)) (m)) -> ((R) (((nat.S) ) (n))) (((nat.S) ) (m))) -> forall (n:nat.nat) , forall (m:nat.nat) , ((R) (n)) (m).

nat_elim2 : LEMMA (FORALL(R:[nat_sttfa.sttfa_nat -> [nat_sttfa.sttfa_nat -> bool]]):((FORALL(n:nat_sttfa.sttfa_nat):R(nat_sttfa.sttfa_O)(n)) => ((FORALL(n:nat_sttfa.sttfa_nat):R(nat_sttfa.sttfa_S(n))(nat_sttfa.sttfa_O)) => ((FORALL(n:nat_sttfa.sttfa_nat):(FORALL(m:nat_sttfa.sttfa_nat):(R(n)(m) => R(nat_sttfa.sttfa_S(n))(nat_sttfa.sttfa_S(m))))) => (FORALL(n:nat_sttfa.sttfa_nat):(FORALL(m:nat_sttfa.sttfa_nat):R(n)(m)))))))

Printing for OpenTheory is not working at the moment.