From 409f569bde067546830df25cd0b1ca898573f66a Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 28 Oct 2011 09:33:44 +0000 Subject: [PATCH] some qed- --- matita/matita/lib/basics/logic.ma | 6 +++--- matita/matita/lib/basics/relations.ma | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma index a3858dfb7..bf3bae3a8 100644 --- a/matita/matita/lib/basics/logic.ma +++ b/matita/matita/lib/basics/logic.ma @@ -1,4 +1,4 @@ -(* + (* ||M|| This file is part of HELM, an Hypertextual, Electronic ||A|| Library of Mathematics, developed at the Computer Science ||T|| Department of the University of Bologna, Italy. @@ -47,7 +47,7 @@ theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y → #A #x #P #Hx #y #Heq (cases Heq); //; qed. theorem sym_eq: ∀A.∀x,y:A. x = y → y = x. -#A #x #y #Heq @(rewrite_l A x (λz.z=x)); //; qed. +#A #x #y #Heq @(rewrite_l A x (λz.z=x)) // qed-. theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y = x → P y. #A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed. @@ -56,7 +56,7 @@ theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B. #A #B #Ha #Heq (elim Heq); //; qed. theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z. -#A #x #y #z #H1 #H2 >H1; //; qed. +#A #x #y #z #H1 #H2 >H1; //; qed-. theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y. #A #B #f #x #y #H >H; //; qed. diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma index b31db23d7..59aad912d 100644 --- a/matita/matita/lib/basics/relations.ma +++ b/matita/matita/lib/basics/relations.ma @@ -73,7 +73,7 @@ definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop lemma injective_compose : ∀A,B,C,f,g. injective A B f → injective B C g → injective A C (λx.g (f x)). -/3/; qed. +/3/; qed-. (* extensional equality *) -- 2.39.2