- some bugs fixed in the domain-based preorders on environments

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Base-1 / types / defs.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
index cddd83fd9d46b1a49dc249f3e40638fd354e850d..6699002d5213df585357544c9bb276d76c469227 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
@@ -38,6 +38,14 @@ inductive or4 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop): Prop \def
 | or4_intro2: P2 \to (or4 P0 P1 P2 P3)
 | or4_intro3: P3 \to (or4 P0 P1 P2 P3).
 
+inductive or5 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop) (P4: Prop): Prop 
+\def
+| or5_intro0: P0 \to (or5 P0 P1 P2 P3 P4)
+| or5_intro1: P1 \to (or5 P0 P1 P2 P3 P4)
+| or5_intro2: P2 \to (or5 P0 P1 P2 P3 P4)
+| or5_intro3: P3 \to (or5 P0 P1 P2 P3 P4)
+| or5_intro4: P4 \to (or5 P0 P1 P2 P3 P4).
+
 inductive ex3 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to 
 Prop): Prop \def
 | ex3_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to (ex3 A0