- we introduced the pointer_step rc in the perspective of proving

[helm.git] / matita / matita / contribs / lambda / pointer_list.ma

diff --git a/matita/matita/contribs/lambda/pointer_list.ma b/matita/matita/contribs/lambda/pointer_list.ma
index 82f704a78e681ac59dd98157019326709be40e1c..becfc0a5ee436a673c33e009c0d7070eb73ff312 100644 (file)
--- 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).