let not_bool =
(function b -> 
(match b with 
   Matita_datatypes_bool.True -> Matita_datatypes_bool.False
 | Matita_datatypes_bool.False -> Matita_datatypes_bool.True)
)
;;

let and_bool =
(function b1 -> (function b2 -> 
(match b1 with 
   Matita_datatypes_bool.True -> b2
 | Matita_datatypes_bool.False -> Matita_datatypes_bool.False)
))
;;

let or_bool =
(function b1 -> (function b2 -> 
(match b1 with 
   Matita_datatypes_bool.True -> Matita_datatypes_bool.True
 | Matita_datatypes_bool.False -> b2)
))
;;

let xor_bool =
(function b1 -> (function b2 -> 
(match b1 with 
   Matita_datatypes_bool.True -> (not_bool b2)
 | Matita_datatypes_bool.False -> b2)
))
;;

let eq_bool =
(function b1 -> (function b2 -> 
(match b1 with 
   Matita_datatypes_bool.True -> b2
 | Matita_datatypes_bool.False -> (not_bool b2))
))
;;

type ('t1,'t2,'t3) prod3T =
TripleT of 't1 * 't2 * 't3
;;

let prod3T_rec =
(function f -> (function p -> 
(match p with 
   TripleT(t,t1,t2) -> (f t t1 t2))
))
;;

let prod3T_rect =
(function f -> (function p -> 
(match p with 
   TripleT(t,t1,t2) -> (f t t1 t2))
))
;;

let fst3T =
(function p -> 
(match p with 
   TripleT(x,_,_) -> x)
)
;;

let snd3T =
(function p -> 
(match p with 
   TripleT(_,x,_) -> x)
)
;;

let thd3T =
(function p -> 
(match p with 
   TripleT(_,_,x) -> x)
)
;;

type ('t1,'t2,'t3,'t4) prod4T =
QuadrupleT of 't1 * 't2 * 't3 * 't4
;;

let prod4T_rec =
(function f -> (function p -> 
(match p with 
   QuadrupleT(t,t1,t2,t3) -> (f t t1 t2 t3))
))
;;

let prod4T_rect =
(function f -> (function p -> 
(match p with 
   QuadrupleT(t,t1,t2,t3) -> (f t t1 t2 t3))
))
;;

let fst4T =
(function p -> 
(match p with 
   QuadrupleT(x,_,_,_) -> x)
)
;;

let snd4T =
(function p -> 
(match p with 
   QuadrupleT(_,x,_,_) -> x)
)
;;

let thd4T =
(function p -> 
(match p with 
   QuadrupleT(_,_,x,_) -> x)
)
;;

let fth4T =
(function p -> 
(match p with 
   QuadrupleT(_,_,_,x) -> x)
)
;;

type ('t1,'t2,'t3,'t4,'t5) prod5T =
QuintupleT of 't1 * 't2 * 't3 * 't4 * 't5
;;

let prod5T_rec =
(function f -> (function p -> 
(match p with 
   QuintupleT(t,t1,t2,t3,t4) -> (f t t1 t2 t3 t4))
))
;;

let prod5T_rect =
(function f -> (function p -> 
(match p with 
   QuintupleT(t,t1,t2,t3,t4) -> (f t t1 t2 t3 t4))
))
;;

let fst5T =
(function p -> 
(match p with 
   QuintupleT(x,_,_,_,_) -> x)
)
;;

let snd5T =
(function p -> 
(match p with 
   QuintupleT(_,x,_,_,_) -> x)
)
;;

let thd5T =
(function p -> 
(match p with 
   QuintupleT(_,_,x,_,_) -> x)
)
;;

let frth5T =
(function p -> 
(match p with 
   QuintupleT(_,_,_,x,_) -> x)
)
;;

let ffth5T =
(function p -> 
(match p with 
   QuintupleT(_,_,_,_,x) -> x)
)
;;

let opt_map =
(function t -> (function f -> 
(match t with 
   Matita_datatypes_constructors.None -> (Matita_datatypes_constructors.None)
 | Matita_datatypes_constructors.Some(x) -> (f x))
))
;;

let nat_of_bool =
(function b -> 
(match b with 
   Matita_datatypes_bool.True -> (Matita_nat_nat.S(Matita_nat_nat.O))
 | Matita_datatypes_bool.False -> Matita_nat_nat.O)
)
;;