X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Frelations.ma;h=753ed32332d9e51f4a09f306ac9b929c103e96d3;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=34d6fe11cd9b9bae04e91bb48aeddce65f554982;hpb=e10f6cc76602309d92af9c831e755dfa5e593b68;p=helm.git

diff --git a/weblib/basics/relations.ma b/weblib/basics/relations.ma
index 34d6fe11c..753ed3233 100644
--- a/weblib/basics/relations.ma
+++ b/weblib/basics/relations.ma
@@ -48,7 +48,7 @@ definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
 ≝ λA,B.λf.∀x,y:A.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f y → xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ay.
 
 definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
-≝λA,B.λf.∀z:B.a title="exists" href="cic:/fakeuri.def(1)"∃/ax:A.z a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x.
+≝λA,B.λf.∀z:B.a title="exists" href="cic:/fakeuri.def(1)"∃/ax:Aa title="exists" href="cic:/fakeuri.def(1)"./az a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x.
 
 definition commutative: ∀A:Type[0].∀f:A→A→A.Prop 
 ≝ λA.λf.∀x,y.f x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f y x.
@@ -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.
 a href="cic:/matita/basics/relations/injective.def(1)"injective/a A B f → a href="cic:/matita/basics/relations/injective.def(1)"injective/a B C g → a href="cic:/matita/basics/relations/injective.def(1)"injective/a A C (λx.g (f x)).
-/3/; qed.
+/span class="autotactic"3span class="autotrace" trace /span/span/; qed.
 
 (* extensional equality *)
 
@@ -102,4 +102,4 @@ notation " f \eqF g " non associative with precedence 45
 for @{'eqF ? ? f g}.
 
 interpretation "functional extentional equality" 
-'eqF A B f g = (exteqF A B f g).
+'eqF A B f g = (exteqF A B f g).
\ No newline at end of file