+(* ex6_7 *)
+
+Inductive ex6_7 [A0,A1,A2,A3,A4,A5,A6:Set; P0,P1,P2,P3,P4,P5:A0->A1->A2->A3->A4->A5->A6->Prop] : Prop :=
+ ex6_7_intro : (x0:A0; x1:A1; x2:A2; x3:A3; x4:A4; x5:A5; x6:A6)(P0 x0 x1 x2 x3 x4 x5 x6)->(P1 x0 x1 x2 x3 x4 x5 x6)->(P2 x0 x1 x2 x3 x4 x5 x6)->(P3 x0 x1 x2 x3 x4 x5 x6)->(P4 x0 x1 x2 x3 x4 x5 x6)->(P5 x0 x1 x2 x3 x4 x5 x6)->(ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5).
+
+Hint ex6_7 : ltlc := Constructors ex6_7.
+
+Syntactic Definition Ex6_7 := ex6_7 | 1.
+
+Grammar constr constr10 :=
+ | ex6_7implicit
+ [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) ident($v4) ident($v5) ident($v6) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) "&" constr($c4) "&" constr($c5) ] ->
+ [ (ex6_7 ? ? ? ? ? ? ? [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c0 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c1 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c2 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c3 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c4 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c5) ].
+
+(* extended Decompose tactic *)
+
+Tactic Definition XDecompose H :=
+ Decompose [and or ex ex2 or3 or4 ex2_2 ex3_2 ex_3 ex3_3 ex4_3 ex3_4 ex4_4 ex4_5 ex5_5 ex6_6 ex6_7] H; Clear H.
+