X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fxoa.ma;h=1a92dbad046c512928465cc6e2a07736a3dbc574;hb=4854493daa451ed14c980665f9901cd8a9dc5fbe;hp=4e6e6aed938067f108fb3777a4d558b5a89a77c5;hpb=2b51cf74b9a5f37d0f91780ceae4b8f4d0ee38a1;p=helm.git

diff --git a/matita/matita/contribs/lambda/xoa.ma b/matita/matita/contribs/lambda/xoa.ma
index 4e6e6aed9..1a92dbad0 100644
--- a/matita/matita/contribs/lambda/xoa.ma
+++ b/matita/matita/contribs/lambda/xoa.ma
@@ -32,3 +32,13 @@ inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝
 
 interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2).
 
+(* multiple disjunction connective (3) *)
+
+inductive or3 (P0,P1,P2:Prop) : Prop ≝
+   | or3_intro0: P0 → or3 ? ? ?
+   | or3_intro1: P1 → or3 ? ? ?
+   | or3_intro2: P2 → or3 ? ? ?
+.
+
+interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2).
+