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 Prop))))))): Prop \def
| ex6_7_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2 x3 x4 x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1 x2 x3 x4 x5 x6) \to ((P3 x0 x1 x2 x3 x4 x5 x6) \to ((P4 x0 x1 x2 x3 x4 x5 x6) \to ((P5 x0 x1 x2 x3 x4 x5 x6) \to (ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5))))))))))))).
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 Prop))))))): Prop \def
| ex6_7_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2 x3 x4 x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1 x2 x3 x4 x5 x6) \to ((P3 x0 x1 x2 x3 x4 x5 x6) \to ((P4 x0 x1 x2 x3 x4 x5 x6) \to ((P5 x0 x1 x2 x3 x4 x5 x6) \to (ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5))))))))))))).