- predefined_virtuals: nwe characters

[helm.git] / matita / matita / contribs / lambda_delta / ground_2 / xoa.ma

diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
index 3d265bc4758b31feaa9578639a5669dabb6ac6c1..f4296024fef1451511b1c4dd6c176d942f572a1a 100644 (file)
--- 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).
+