- \lambda (S: Set).(\lambda (x: S).(\lambda (P: ((S \to Prop))).(\lambda (G:
-((S \to Prop))).(\lambda (H: ((\forall (y: S).((P y) \to ((eq S y x) \to (G
-y)))))).(\lambda (H0: (P x)).(H x H0 (refl_equal S x))))))).
-(* COMMENTS
-Initial nodes: 45
-END *)
+ \lambda (S: Type[0]).(\lambda (x: S).(\lambda (P: ((S \to Prop))).(\lambda
+(G: ((S \to Prop))).(\lambda (H: ((\forall (y: S).((P y) \to ((eq S y x) \to
+(G y)))))).(\lambda (H0: (P x)).(H x H0 (refl_equal S x))))))).