X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBase-1%2Ftypes%2Fdefs.ma;h=6699002d5213df585357544c9bb276d76c469227;hb=f73bd1c1cdd504c2a991071505b2e4f541791a7f;hp=cddd83fd9d46b1a49dc249f3e40638fd354e850d;hpb=eccaad18aa815bb3334e205b97c220f675e6d5a5;p=helm.git

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 cddd83fd9..6699002d5 100644
--- 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