4 Matita_datatypes_bool.True -> Matita_datatypes_bool.False
5 | Matita_datatypes_bool.False -> Matita_datatypes_bool.True)
10 (function b1 -> (function b2 ->
12 Matita_datatypes_bool.True -> b2
13 | Matita_datatypes_bool.False -> Matita_datatypes_bool.False)
18 (function b1 -> (function b2 ->
20 Matita_datatypes_bool.True -> Matita_datatypes_bool.True
21 | Matita_datatypes_bool.False -> b2)
26 (function b1 -> (function b2 ->
28 Matita_datatypes_bool.True -> (not_bool b2)
29 | Matita_datatypes_bool.False -> b2)
34 (function b1 -> (function b2 ->
36 Matita_datatypes_bool.True -> b2
37 | Matita_datatypes_bool.False -> (not_bool b2))
41 type ('t1,'t2,'t3) prod3T =
42 TripleT of 't1 * 't2 * 't3
46 (function f -> (function p ->
48 TripleT(t,t1,t2) -> (f t t1 t2))
53 (function f -> (function p ->
55 TripleT(t,t1,t2) -> (f t t1 t2))
80 type ('t1,'t2,'t3,'t4) prod4T =
81 QuadrupleT of 't1 * 't2 * 't3 * 't4
85 (function f -> (function p ->
87 QuadrupleT(t,t1,t2,t3) -> (f t t1 t2 t3))
92 (function f -> (function p ->
94 QuadrupleT(t,t1,t2,t3) -> (f t t1 t2 t3))
101 QuadrupleT(x,_,_,_) -> x)
108 QuadrupleT(_,x,_,_) -> x)
115 QuadrupleT(_,_,x,_) -> x)
122 QuadrupleT(_,_,_,x) -> x)
126 type ('t1,'t2,'t3,'t4,'t5) prod5T =
127 QuintupleT of 't1 * 't2 * 't3 * 't4 * 't5
131 (function f -> (function p ->
133 QuintupleT(t,t1,t2,t3,t4) -> (f t t1 t2 t3 t4))
138 (function f -> (function p ->
140 QuintupleT(t,t1,t2,t3,t4) -> (f t t1 t2 t3 t4))
147 QuintupleT(x,_,_,_,_) -> x)
154 QuintupleT(_,x,_,_,_) -> x)
161 QuintupleT(_,_,x,_,_) -> x)
168 QuintupleT(_,_,_,x,_) -> x)
175 QuintupleT(_,_,_,_,x) -> x)
180 (function t -> (function f ->
182 Matita_datatypes_constructors.None -> (Matita_datatypes_constructors.None)
183 | Matita_datatypes_constructors.Some(x) -> (f x))
190 Matita_datatypes_bool.True -> (Matita_nat_nat.S(Matita_nat_nat.O))
191 | Matita_datatypes_bool.False -> Matita_nat_nat.O)