(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

(* This file was generated by coqgen *)

Require bg_require.

(* builtin decomposables *)

Hint True : ld := Constructors True.

Hint and : ld := Constructors and.

Hint ex : ld := Constructors ex.

Hint ex2 : ld := Constructors ex2.

Hint or : ld := Constructors or.

(* extensions for ex2 *)

(*#* #stop file *)

Syntactic Definition ex2_intro := ex_intro2.

(*#* #start file *)

(* and3 *)

Inductive and3 [P0,P1,P2:Prop] : Prop :=
   | and3_intro : P0 -> P1 -> P2 -> (and3 P0 P1 P2).

Hint and3 : ld := Constructors and3.

(*#* #stop file *)

Grammar constr constr10 :=
   | and3
      [ "AND" constr($c0) "&" constr($c1) "&" constr($c2) ] ->
      [ (and3 $c0 $c1 $c2) ].

(*#* #start file *)

(* and4 *)

Inductive and4 [P0,P1,P2,P3:Prop] : Prop :=
   | and4_intro : P0 -> P1 -> P2 -> P3 -> (and4 P0 P1 P2 P3).

Hint and4 : ld := Constructors and4.

(*#* #stop file *)

Grammar constr constr10 :=
   | and4
      [ "AND" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) ] ->
      [ (and4 $c0 $c1 $c2 $c3) ].

(*#* #start file *)

(* and5 *)

Inductive and5 [P0,P1,P2,P3,P4:Prop] : Prop :=
   | and5_intro : P0 -> P1 -> P2 -> P3 -> P4 -> (and5 P0 P1 P2 P3 P4).

Hint and5 : ld := Constructors and5.

(*#* #stop file *)

Grammar constr constr10 :=
   | and5
      [ "AND" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) "&" constr($c4) ] ->
      [ (and5 $c0 $c1 $c2 $c3 $c4) ].

(*#* #start file *)

(* or3 *)

Inductive or3 [P0,P1,P2:Prop] : Prop :=
   | or3_intro0 : P0 -> (or3 P0 P1 P2)
   | or3_intro1 : P1 -> (or3 P0 P1 P2)
   | or3_intro2 : P2 -> (or3 P0 P1 P2).

Hint or3 : ld := Constructors or3.

(*#* #stop file *)

Grammar constr constr10 :=
   | or3
      [ "OR" constr($c0) "|" constr($c1) "|" constr($c2) ] ->
      [ (or3 $c0 $c1 $c2) ].

(*#* #start file *)

(* or4 *)

Inductive or4 [P0,P1,P2,P3:Prop] : Prop :=
   | or4_intro0 : P0 -> (or4 P0 P1 P2 P3)
   | or4_intro1 : P1 -> (or4 P0 P1 P2 P3)
   | or4_intro2 : P2 -> (or4 P0 P1 P2 P3)
   | or4_intro3 : P3 -> (or4 P0 P1 P2 P3).

Hint or4 : ld := Constructors or4.

(*#* #stop file *)

Grammar constr constr10 :=
   | or4
      [ "OR" constr($c0) "|" constr($c1) "|" constr($c2) "|" constr($c3) ] ->
      [ (or4 $c0 $c1 $c2 $c3) ].

(*#* #start file *)

(* or5 *)

Inductive or5 [P0,P1,P2,P3,P4:Prop] : Prop :=
   | or5_intro0 : P0 -> (or5 P0 P1 P2 P3 P4)
   | or5_intro1 : P1 -> (or5 P0 P1 P2 P3 P4)
   | or5_intro2 : P2 -> (or5 P0 P1 P2 P3 P4)
   | or5_intro3 : P3 -> (or5 P0 P1 P2 P3 P4)
   | or5_intro4 : P4 -> (or5 P0 P1 P2 P3 P4).

Hint or5 : ld := Constructors or5.

(*#* #stop file *)

Grammar constr constr10 :=
   | or5
      [ "OR" constr($c0) "|" constr($c1) "|" constr($c2) "|" constr($c3) "|" constr($c4) ] ->
      [ (or5 $c0 $c1 $c2 $c3 $c4) ].

(*#* #start file *)

(* ex3 *)

Inductive ex3 [A0:Set; P0,P1,P2:A0->Prop] : Prop :=
   | ex3_intro : (x0:A0)(P0 x0)->(P1 x0)->(P2 x0)->(ex3 A0 P0 P1 P2).

Hint ex3 : ld := Constructors ex3.

(*#* #stop file *)

Syntactic Definition Ex3 := ex3 | 1.

Grammar constr constr10 :=
   | ex3implicit
      [ "EX" ident($v0) "|" constr($c0) "&" constr($c1) "&" constr($c2) ] ->
      [ (ex3 ? [$v0]$c0 [$v0]$c1 [$v0]$c2) ].

(*#* #start file *)

(* ex4 *)

Inductive ex4 [A0:Set; P0,P1,P2,P3:A0->Prop] : Prop :=
   | ex4_intro : (x0:A0)(P0 x0)->(P1 x0)->(P2 x0)->(P3 x0)->(ex4 A0 P0 P1 P2 P3).

Hint ex4 : ld := Constructors ex4.

(*#* #stop file *)

Syntactic Definition Ex4 := ex4 | 1.

Grammar constr constr10 :=
   | ex4implicit
      [ "EX" ident($v0) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) ] ->
      [ (ex4 ? [$v0]$c0 [$v0]$c1 [$v0]$c2 [$v0]$c3) ].

(*#* #start file *)

(* ex_2 *)

Inductive ex_2 [A0,A1:Set; P0:A0->A1->Prop] : Prop :=
   | ex_2_intro : (x0:A0; x1:A1)(P0 x0 x1)->(ex_2 A0 A1 P0).

Hint ex_2 : ld := Constructors ex_2.

(*#* #stop file *)

Syntactic Definition Ex_2 := ex_2 | 1.

Grammar constr constr10 :=
   | ex_2implicit
      [ "EX" ident($v0) ident($v1) "|" constr($c0) ] ->
      [ (ex_2 ? ? [$v0;$v1]$c0) ].

(*#* #start file *)

(* ex2_2 *)

Inductive ex2_2 [A0,A1:Set; P0,P1:A0->A1->Prop] : Prop :=
   | ex2_2_intro : (x0:A0; x1:A1)(P0 x0 x1)->(P1 x0 x1)->(ex2_2 A0 A1 P0 P1).

Hint ex2_2 : ld := Constructors ex2_2.

(*#* #stop file *)

Syntactic Definition Ex2_2 := ex2_2 | 1.

Grammar constr constr10 :=
   | ex2_2implicit
      [ "EX" ident($v0) ident($v1) "|" constr($c0) "&" constr($c1) ] ->
      [ (ex2_2 ? ? [$v0;$v1]$c0 [$v0;$v1]$c1) ].

(*#* #start file *)

(* ex3_2 *)

Inductive ex3_2 [A0,A1:Set; P0,P1,P2:A0->A1->Prop] : Prop :=
   | ex3_2_intro : (x0:A0; x1:A1)(P0 x0 x1)->(P1 x0 x1)->(P2 x0 x1)->(ex3_2 A0 A1 P0 P1 P2).

Hint ex3_2 : ld := Constructors ex3_2.

(*#* #stop file *)

Syntactic Definition Ex3_2 := ex3_2 | 1.

Grammar constr constr10 :=
   | ex3_2implicit
      [ "EX" ident($v0) ident($v1) "|" constr($c0) "&" constr($c1) "&" constr($c2) ] ->
      [ (ex3_2 ? ? [$v0;$v1]$c0 [$v0;$v1]$c1 [$v0;$v1]$c2) ].

(*#* #start file *)

(* ex4_2 *)

Inductive ex4_2 [A0,A1:Set; P0,P1,P2,P3:A0->A1->Prop] : Prop :=
   | ex4_2_intro : (x0:A0; x1:A1)(P0 x0 x1)->(P1 x0 x1)->(P2 x0 x1)->(P3 x0 x1)->(ex4_2 A0 A1 P0 P1 P2 P3).

Hint ex4_2 : ld := Constructors ex4_2.

(*#* #stop file *)

Syntactic Definition Ex4_2 := ex4_2 | 1.

Grammar constr constr10 :=
   | ex4_2implicit
      [ "EX" ident($v0) ident($v1) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) ] ->
      [ (ex4_2 ? ? [$v0;$v1]$c0 [$v0;$v1]$c1 [$v0;$v1]$c2 [$v0;$v1]$c3) ].

(*#* #start file *)

(* ex_3 *)

Inductive ex_3 [A0,A1,A2:Set; P0:A0->A1->A2->Prop] : Prop :=
   | ex_3_intro : (x0:A0; x1:A1; x2:A2)(P0 x0 x1 x2)->(ex_3 A0 A1 A2 P0).

Hint ex_3 : ld := Constructors ex_3.

(*#* #stop file *)

Syntactic Definition Ex_3 := ex_3 | 1.

Grammar constr constr10 :=
   | ex_3implicit
      [ "EX" ident($v0) ident($v1) ident($v2) "|" constr($c0) ] ->
      [ (ex_3 ? ? ? [$v0;$v1;$v2]$c0) ].

(*#* #start file *)

(* ex2_3 *)

Inductive ex2_3 [A0,A1,A2:Set; P0,P1:A0->A1->A2->Prop] : Prop :=
   | ex2_3_intro : (x0:A0; x1:A1; x2:A2)(P0 x0 x1 x2)->(P1 x0 x1 x2)->(ex2_3 A0 A1 A2 P0 P1).

Hint ex2_3 : ld := Constructors ex2_3.

(*#* #stop file *)

Syntactic Definition Ex2_3 := ex2_3 | 1.

Grammar constr constr10 :=
   | ex2_3implicit
      [ "EX" ident($v0) ident($v1) ident($v2) "|" constr($c0) "&" constr($c1) ] ->
      [ (ex2_3 ? ? ? [$v0;$v1;$v2]$c0 [$v0;$v1;$v2]$c1) ].

(*#* #start file *)

(* ex3_3 *)

Inductive ex3_3 [A0,A1,A2:Set; P0,P1,P2:A0->A1->A2->Prop] : Prop :=
   | ex3_3_intro : (x0:A0; x1:A1; x2:A2)(P0 x0 x1 x2)->(P1 x0 x1 x2)->(P2 x0 x1 x2)->(ex3_3 A0 A1 A2 P0 P1 P2).

Hint ex3_3 : ld := Constructors ex3_3.

(*#* #stop file *)

Syntactic Definition Ex3_3 := ex3_3 | 1.

Grammar constr constr10 :=
   | ex3_3implicit
      [ "EX" ident($v0) ident($v1) ident($v2) "|" constr($c0) "&" constr($c1) "&" constr($c2) ] ->
      [ (ex3_3 ? ? ? [$v0;$v1;$v2]$c0 [$v0;$v1;$v2]$c1 [$v0;$v1;$v2]$c2) ].

(*#* #start file *)

(* ex4_3 *)

Inductive ex4_3 [A0,A1,A2:Set; P0,P1,P2,P3:A0->A1->A2->Prop] : Prop :=
   | ex4_3_intro : (x0:A0; x1:A1; x2:A2)(P0 x0 x1 x2)->(P1 x0 x1 x2)->(P2 x0 x1 x2)->(P3 x0 x1 x2)->(ex4_3 A0 A1 A2 P0 P1 P2 P3).

Hint ex4_3 : ld := Constructors ex4_3.

(*#* #stop file *)

Syntactic Definition Ex4_3 := ex4_3 | 1.

Grammar constr constr10 :=
   | ex4_3implicit
      [ "EX" ident($v0) ident($v1) ident($v2) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) ] ->
      [ (ex4_3 ? ? ? [$v0;$v1;$v2]$c0 [$v0;$v1;$v2]$c1 [$v0;$v1;$v2]$c2 [$v0;$v1;$v2]$c3) ].

(*#* #start file *)

(* ex5_3 *)

Inductive ex5_3 [A0,A1,A2:Set; P0,P1,P2,P3,P4:A0->A1->A2->Prop] : Prop :=
   | ex5_3_intro : (x0:A0; x1:A1; x2:A2)(P0 x0 x1 x2)->(P1 x0 x1 x2)->(P2 x0 x1 x2)->(P3 x0 x1 x2)->(P4 x0 x1 x2)->(ex5_3 A0 A1 A2 P0 P1 P2 P3 P4).

Hint ex5_3 : ld := Constructors ex5_3.

(*#* #stop file *)

Syntactic Definition Ex5_3 := ex5_3 | 1.

Grammar constr constr10 :=
   | ex5_3implicit
      [ "EX" ident($v0) ident($v1) ident($v2) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) "&" constr($c4) ] ->
      [ (ex5_3 ? ? ? [$v0;$v1;$v2]$c0 [$v0;$v1;$v2]$c1 [$v0;$v1;$v2]$c2 [$v0;$v1;$v2]$c3 [$v0;$v1;$v2]$c4) ].

(*#* #start file *)

(* ex3_4 *)

Inductive ex3_4 [A0,A1,A2,A3:Set; P0,P1,P2:A0->A1->A2->A3->Prop] : Prop :=
   | ex3_4_intro : (x0:A0; x1:A1; x2:A2; x3:A3)(P0 x0 x1 x2 x3)->(P1 x0 x1 x2 x3)->(P2 x0 x1 x2 x3)->(ex3_4 A0 A1 A2 A3 P0 P1 P2).

Hint ex3_4 : ld := Constructors ex3_4.

(*#* #stop file *)

Syntactic Definition Ex3_4 := ex3_4 | 1.

Grammar constr constr10 :=
   | ex3_4implicit
      [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) "|" constr($c0) "&" constr($c1) "&" constr($c2) ] ->
      [ (ex3_4 ? ? ? ? [$v0;$v1;$v2;$v3]$c0 [$v0;$v1;$v2;$v3]$c1 [$v0;$v1;$v2;$v3]$c2) ].

(*#* #start file *)

(* ex4_4 *)

Inductive ex4_4 [A0,A1,A2,A3:Set; P0,P1,P2,P3:A0->A1->A2->A3->Prop] : Prop :=
   | ex4_4_intro : (x0:A0; x1:A1; x2:A2; x3:A3)(P0 x0 x1 x2 x3)->(P1 x0 x1 x2 x3)->(P2 x0 x1 x2 x3)->(P3 x0 x1 x2 x3)->(ex4_4 A0 A1 A2 A3 P0 P1 P2 P3).

Hint ex4_4 : ld := Constructors ex4_4.

(*#* #stop file *)

Syntactic Definition Ex4_4 := ex4_4 | 1.

Grammar constr constr10 :=
   | ex4_4implicit
      [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) ] ->
      [ (ex4_4 ? ? ? ? [$v0;$v1;$v2;$v3]$c0 [$v0;$v1;$v2;$v3]$c1 [$v0;$v1;$v2;$v3]$c2 [$v0;$v1;$v2;$v3]$c3) ].

(*#* #start file *)

(* ex4_5 *)

Inductive ex4_5 [A0,A1,A2,A3,A4:Set; P0,P1,P2,P3:A0->A1->A2->A3->A4->Prop] : Prop :=
   | ex4_5_intro : (x0:A0; x1:A1; x2:A2; x3:A3; x4:A4)(P0 x0 x1 x2 x3 x4)->(P1 x0 x1 x2 x3 x4)->(P2 x0 x1 x2 x3 x4)->(P3 x0 x1 x2 x3 x4)->(ex4_5 A0 A1 A2 A3 A4 P0 P1 P2 P3).

Hint ex4_5 : ld := Constructors ex4_5.

(*#* #stop file *)

Syntactic Definition Ex4_5 := ex4_5 | 1.

Grammar constr constr10 :=
   | ex4_5implicit
      [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) ident($v4) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) ] ->
      [ (ex4_5 ? ? ? ? ? [$v0;$v1;$v2;$v3;$v4]$c0 [$v0;$v1;$v2;$v3;$v4]$c1 [$v0;$v1;$v2;$v3;$v4]$c2 [$v0;$v1;$v2;$v3;$v4]$c3) ].

(*#* #start file *)

(* ex5_5 *)

Inductive ex5_5 [A0,A1,A2,A3,A4:Set; P0,P1,P2,P3,P4:A0->A1->A2->A3->A4->Prop] : Prop :=
   | ex5_5_intro : (x0:A0; x1:A1; x2:A2; x3:A3; x4:A4)(P0 x0 x1 x2 x3 x4)->(P1 x0 x1 x2 x3 x4)->(P2 x0 x1 x2 x3 x4)->(P3 x0 x1 x2 x3 x4)->(P4 x0 x1 x2 x3 x4)->(ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4).

Hint ex5_5 : ld := Constructors ex5_5.

(*#* #stop file *)

Syntactic Definition Ex5_5 := ex5_5 | 1.

Grammar constr constr10 :=
   | ex5_5implicit
      [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) ident($v4) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) "&" constr($c4) ] ->
      [ (ex5_5 ? ? ? ? ? [$v0;$v1;$v2;$v3;$v4]$c0 [$v0;$v1;$v2;$v3;$v4]$c1 [$v0;$v1;$v2;$v3;$v4]$c2 [$v0;$v1;$v2;$v3;$v4]$c3 [$v0;$v1;$v2;$v3;$v4]$c4) ].

(*#* #start file *)

(* ex6_6 *)

Inductive ex6_6 [A0,A1,A2,A3,A4,A5:Set; P0,P1,P2,P3,P4,P5:A0->A1->A2->A3->A4->A5->Prop] : Prop :=
   | ex6_6_intro : (x0:A0; x1:A1; x2:A2; x3:A3; x4:A4; x5:A5)(P0 x0 x1 x2 x3 x4 x5)->(P1 x0 x1 x2 x3 x4 x5)->(P2 x0 x1 x2 x3 x4 x5)->(P3 x0 x1 x2 x3 x4 x5)->(P4 x0 x1 x2 x3 x4 x5)->(P5 x0 x1 x2 x3 x4 x5)->(ex6_6 A0 A1 A2 A3 A4 A5 P0 P1 P2 P3 P4 P5).

Hint ex6_6 : ld := Constructors ex6_6.

(*#* #stop file *)

Syntactic Definition Ex6_6 := ex6_6 | 1.

Grammar constr constr10 :=
   | ex6_6implicit
      [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) ident($v4) ident($v5) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) "&" constr($c4) "&" constr($c5) ] ->
      [ (ex6_6 ? ? ? ? ? ? [$v0;$v1;$v2;$v3;$v4;$v5]$c0 [$v0;$v1;$v2;$v3;$v4;$v5]$c1 [$v0;$v1;$v2;$v3;$v4;$v5]$c2 [$v0;$v1;$v2;$v3;$v4;$v5]$c3 [$v0;$v1;$v2;$v3;$v4;$v5]$c4 [$v0;$v1;$v2;$v3;$v4;$v5]$c5) ].

(*#* #start file *)

(* 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 : ld := Constructors ex6_7.

(*#* #stop file *)

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) ].

(*#* #start file *)

(* extended Decompose tactic *)

(*#* #stop file *)

Tactic Definition XDecompose H :=
   Simpl in H; Decompose [False and or ex ex2 and3 and4 and5 or3 or4 or5 ex3 ex4 ex_2 ex2_2 ex3_2 ex4_2 ex_3 ex2_3 ex3_3 ex4_3 ex5_3 ex3_4 ex4_4 ex4_5 ex5_5 ex6_6 ex6_7] H; Clear H.

Tactic Definition XDecomPose t :=
   XPose H_x t; XDecompose H_x.

Tactic Definition XDecomPoseClear H t :=
   XDecomPose t; Clear H.

(*#* #start file *)