From 841ed2d52ac7276350bffe6bc29df1d762686c17 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 23 Dec 2014 11:58:18 +0000 Subject: [PATCH] check removed --- matita/matita/lib/tutorial/chapter2.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matita/matita/lib/tutorial/chapter2.ma b/matita/matita/lib/tutorial/chapter2.ma index 502e59a40..1f0244505 100644 --- a/matita/matita/lib/tutorial/chapter2.ma +++ b/matita/matita/lib/tutorial/chapter2.ma @@ -383,7 +383,7 @@ inductive Pari : nat → Prop ≝ definition natPari ≝ Sub nat Pari. definition addPari: natPari → natPari → natPari. -* #a #Ha * #b #Hb check mk_Sub @(mk_Sub … (add a b)) +* #a #Ha * #b #Hb @(mk_Sub … (add a b)) elim Ha [normalize @Hb |#x #Hx #Hind normalize @pari2 @Hind -- 2.39.2