-inductive ex6_7 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (A5: Set)
-(A6: Set) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop))))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop))))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop))))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop))))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop))))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
+inductive ex6_7 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (A4:
+Type[0]) (A5: Type[0]) (A6: Type[0]) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4
+\to (A5 \to (A6 \to Prop))))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
+(A5 \to (A6 \to Prop))))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5
+\to (A6 \to Prop))))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to
+(A6 \to Prop))))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6
+\to Prop))))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to