X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpointer_list.ma;h=becfc0a5ee436a673c33e009c0d7070eb73ff312;hb=cbbbc763dc971b43fe74f1d08b797de5d1dc4f17;hp=82f704a78e681ac59dd98157019326709be40e1c;hpb=4bb6799d029b7b377f7aa28b0e90f0a69c149a9c;p=helm.git

diff --git a/matita/matita/contribs/lambda/pointer_list.ma b/matita/matita/contribs/lambda/pointer_list.ma
index 82f704a78..becfc0a5e 100644
--- a/matita/matita/contribs/lambda/pointer_list.ma
+++ b/matita/matita/contribs/lambda/pointer_list.ma
@@ -33,7 +33,7 @@ lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s).
 qed.
 
 definition ho_compatible_rc: predicate (ptrl→relation term) ≝ λR.
-                             ∀s,A1,A2. R s A1 A2 → R (sn:::s) (𝛌.A1) (𝛌.A2).
+                             ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2).
 
 definition ho_compatible_sn: predicate (ptrl→relation term) ≝ λR.
                              ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A).