X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Frelations.ma;h=59aad912df75b687b4c2ebe7481dc2e9f5ca0a47;hb=409f569bde067546830df25cd0b1ca898573f66a;hp=b31db23d7ffffa2e8e6888311194c70ce73b3029;hpb=b78de5584633b864248519d9f7cd9f86a0005c24;p=helm.git

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 *)