- support for candidates of reducibility continues ...

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / computation / lsubc.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma
index 8cf302dc8a7645063ce55c2e7c51d185616e8144..9d38f25d7be95f2db7b89ff3c113fbb9d5dca41a 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma
@@ -16,21 +16,21 @@ include "Basic_2/computation/acp_cr.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
 
-inductive lsubc (R:lenv→predicate term) : relation lenv ≝
-| lsubc_atom: lsubc R (⋆) (⋆)
-| lsubc_pair: ∀I,L1,L2,V. lsubc R L1 L2 → lsubc R (L1. 𝕓{I} V) (L2. 𝕓{I} V)
-| lsubc_abbr: ∀L1,L2,V,W,A. R ⊢ {L1, V} ϵ 〚A〛 → R ⊢ {L2, W} ϵ 〚A〛 →
-              lsubc R L1 L2 → lsubc R (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W)
+inductive lsubc (RP:lenv→predicate term): relation lenv ≝
+| lsubc_atom: lsubc RP (⋆) (⋆)
+| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. 𝕓{I} V) (L2. 𝕓{I} V)
+| lsubc_abbr: ∀L1,L2,V,W,A. {L1, V} [RP] ϵ 〚A〛 → {L2, W} [RP] ϵ 〚A〛 →
+              lsubc RP L1 L2 → lsubc RP (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W)
 .
 
 interpretation
   "local environment refinement (abstract candidates of reducibility)"
-  'CrSubEq L1 R L2 = (lsubc R L1 L2).
+  'CrSubEq L1 RP L2 = (lsubc RP L1 L2).
 
 (* Basic properties *********************************************************)
 
-lemma lsubc_refl: ∀R,L. L [R] ⊑ L.
-#R #L elim L -L // /2 width=1/
+lemma lsubc_refl: ∀RP,L. L [RP] ⊑ L.
+#RP #L elim L -L // /2 width=1/
 qed.
 
 (* Basic inversion lemmas ***************************************************)