- pointer structure simplified

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

diff --git a/matita/matita/contribs/lambda/pointer_sequence.ma b/matita/matita/contribs/lambda/pointer_sequence.ma
index 9f4e63cd6e4f9dd0b6048c2ede1947447c5fcdcf..0a3d3422c37a98cbce8316b4c5c162158f82f19b 100644 (file)
--- a/matita/matita/contribs/lambda/pointer_sequence.ma
+++ b/matita/matita/contribs/lambda/pointer_sequence.ma
@@ -57,7 +57,7 @@ theorem is_head_is_le_trans: ∀r. is_head r → ∀s. is_le s → is_le (r@s).
 qed.
 
 definition ho_compatible_rc: predicate (pseq→relation term) ≝ λR.
-                             ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2).
+                             ∀s,A1,A2. R s A1 A2 → R (sn:::s) (𝛌.A1) (𝛌.A2).
 
 definition ho_compatible_sn: predicate (pseq→relation term) ≝ λR.
                              ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A).