X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=weblib%2Ftutorial%2Fchapter2.ma;fp=weblib%2Ftutorial%2Fchapter2.ma;h=3b878a63c49c3a093b55373ce9584c8f8658cb2f;hb=558e48d29ac55348e4c79103fdd64336a7e69dd1;hp=21a0151cd2f4b17aac12bc916f9a95a28291a241;hpb=2121ee85f036b9554d071bdde1e12af572cc8037;p=helm.git

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 21a0151cd..3b878a63c 100644
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -215,6 +215,13 @@ an element of a of type A and a proof of P(a). The crucial point is to have a la
 reach enough to comprise proofs among its expressions. 
 *)
 
-axiom div2P n : nat → {N×N | True}.
+inductive Sub (A:Type[0]) (P:A → Prop) : Type[0] ≝
+| sub_intro : ∀a:A. P a → Sub A P.
+
+
+
+
+ axiom div2P n : nat → {N×N | True}.
+