X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fground_2%2Fxoa.ma;h=f4296024fef1451511b1c4dd6c176d942f572a1a;hb=53f874fba5b9c39a788085515a4fefe5d29281da;hp=3d265bc4758b31feaa9578639a5669dabb6ac6c1;hpb=a2144f09d1bd7022c1f2dfd4909a1fb9772c8d56;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
index 3d265bc47..f4296024f 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
@@ -221,3 +221,11 @@ inductive and3 (P0,P1,P2:Prop) : Prop ≝
 
 interpretation "multiple conjunction connective (3)" 'And P0 P1 P2 = (and3 P0 P1 P2).
 
+(* multiple conjunction connective (4) *)
+
+inductive and4 (P0,P1,P2,P3:Prop) : Prop ≝
+   | and4_intro: P0 → P1 → P2 → P3 → and4 ? ? ? ?
+.
+
+interpretation "multiple conjunction connective (4)" 'And P0 P1 P2 P3 = (and4 P0 P1 P2 P3).
+