-theorem s_inj:
- \forall (k: K).(\forall (i: nat).(\forall (j: nat).((eq nat (s k i) (s k j))
-\to (eq nat i j))))
-\def
- \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j:
-nat).((eq nat (s k0 i) (s k0 j)) \to (eq nat i j))))) (\lambda (b:
-B).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (eq nat (s (Bind b) i) (s
-(Bind b) j))).(eq_add_S i j H))))) (\lambda (f: F).(\lambda (i: nat).(\lambda
-(j: nat).(\lambda (H: (eq nat (s (Flat f) i) (s (Flat f) j))).H)))) k).
-(* COMMENTS
-Initial nodes: 97
-END *)
-
-theorem s_inc: