From 558e48d29ac55348e4c79103fdd64336a7e69dd1 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 12 Oct 2011 14:00:06 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter2.ma | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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}. + -- 2.39.2