From: Claudio Sacerdoti Coen Date: Wed, 2 Nov 2011 12:57:20 +0000 (+0000) Subject: trans_eq and sym_eq indexing restored. Apparently they are useful for several(?) X-Git-Tag: make_still_working~2141 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dfb3cbe30eacd2c1b333faa3e0d92c3278c24d3c;p=helm.git trans_eq and sym_eq indexing restored. Apparently they are useful for several(?) theorems in CerCo (file positive.ma). --- diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma index bf3bae3a8..2fbe45f37 100644 --- a/matita/matita/lib/basics/logic.ma +++ b/matita/matita/lib/basics/logic.ma @@ -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.