- contex-free normal forms started

[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 2b7af45037e4cdf9738b9647399aa57128819f91..2b75c902d50524eefadcd5f8647f6e14d8afc7bf 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma
@@ -141,3 +141,11 @@ inductive or4 (P0,P1,P2,P3:Prop) : Prop ≝
 
 interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3).
 
+(* multiple conjunction connective (3) *)
+
+inductive and3 (P0,P1,P2:Prop) : Prop ≝
+   | and3_intro: P0 → P1 → P2 → and3 ? ? ?
+.
+
+interpretation "multiple conjunction connective (3)" 'And P0 P1 P2 = (and3 P0 P1 P2).
+