context-free parallel reduction on closures is confluent!

[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 afb5d5aae05515a1c9801c45abb9064f2a55a91f..57403f35698436ae1d8defc9e5fdf02257d678cb 100644 (file)
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -161,5 +161,5 @@ interpretation "functional extentional equality"
 definition bi_relation: Type[0] → Type[0] → Type[0]
 ≝ λA,B.A→B→A→B→Prop.
 
-definition bi_reflexive: ∀A,B. ∀R :bi_relation A B. Prop
+definition bi_reflexive: ∀A,B. ∀R:bi_relation A B. Prop
 ≝ λA,B,R. ∀x,y. R x y x y.