some qed-

[helm.git] / matita / matita / lib / basics / relations.ma

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index b31db23d7ffffa2e8e6888311194c70ce73b3029..59aad912df75b687b4c2ebe7481dc2e9f5ca0a47 100644 (file)
--- 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 *)