X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_equivalence%2Fcpcs.ma;h=22d3b8ebf7abbecc41cdbb4c9b03a0b636dd9dfb;hp=8fc12c258ccdc90299c575cb263544e950806240;hb=c903bdd93123e6fc2ad63a951024da80c9c28307;hpb=cac0166656e08399eaaf1a1e19f0ccea28c36d39

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma
index 8fc12c258..22d3b8ebf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma
@@ -18,8 +18,8 @@ include "basic_2/rt_conversion/cpc.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************)
 
-definition cpcs: sh → relation4 genv lenv term term ≝
-           λh,G. CTC … (cpc h G).
+definition cpcs (h) (G): relation3 lenv term term ≝
+                         CTC … (cpc h G).
 
 interpretation "context-sensitive parallel r-equivalence (term)"
    'PConvStar h G L T1 T2 = (cpcs h G L T1 T2).
@@ -27,69 +27,77 @@ interpretation "context-sensitive parallel r-equivalence (term)"
 (* Basic eliminators ********************************************************)
 
 (* Basic_2A1: was: cpcs_ind_dx *)
-lemma cpcs_ind_sn (h): ∀G,L,T2. ∀R:predicate term. R T2 →
-                       (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → R T → R T1) →
-                       ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T1.
+lemma cpcs_ind_sn (h) (G) (L) (T2):
+                  ∀R:predicate term. R T2 →
+                  (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → R T → R T1) →
+                  ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T1.
 normalize /3 width=6 by TC_star_ind_dx/
 qed-.
 
 (* Basic_2A1: was: cpcs_ind *)
-lemma cpcs_ind_dx (h): ∀G,L,T1. ∀R:predicate term. R T1 →
-                       (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → R T → R T2) →
-                       ∀T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T2.
+lemma cpcs_ind_dx (h) (G) (L) (T1):
+                  ∀R:predicate term. R T1 →
+                  (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → R T → R T2) →
+                  ∀T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T2.
 normalize /3 width=6 by TC_star_ind/
 qed-.
 
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: pc3_refl *)
-lemma cpcs_refl (h): ∀G. c_reflexive … (cpcs h G).
+lemma cpcs_refl (h) (G): c_reflexive … (cpcs h G).
 /2 width=1 by inj/ qed.
 
 (* Basic_1: was: pc3_s *)
-lemma cpcs_sym (h): ∀G,L. symmetric … (cpcs h G L).
+lemma cpcs_sym (h) (G) (L): symmetric … (cpcs h G L).
 #h #G #L @TC_symmetric
 /2 width=1 by cpc_sym/
 qed-.
 
-lemma cpc_cpcs (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+lemma cpc_cpcs (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
 /2 width=1 by inj/ qed.
 
 (* Basic_2A1: was: cpcs_strap2 *)
-lemma cpcs_step_sn (h): ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+lemma cpcs_step_sn (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T →
+                                ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
 normalize /2 width=3 by TC_strap/
 qed-.
 
 (* Basic_2A1: was: cpcs_strap1 *)
-lemma cpcs_step_dx (h): ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+lemma cpcs_step_dx (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T →
+                                ∀T2. ⦃G, L⦄ ⊢ T ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
 normalize /2 width=3 by step/
 qed-.
 
 (* Basic_1: was: pc3_pr2_r *)
-lemma cpr_cpcs_dx (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+lemma cpr_cpcs_dx (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
 /3 width=1 by cpc_cpcs, or_introl/ qed.
 
 (* Basic_1: was: pc3_pr2_x *)
-lemma cpr_cpcs_sn (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡[h] T1 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+lemma cpr_cpcs_sn (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T2 ➡[h] T1 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
 /3 width=1 by cpc_cpcs, or_intror/ qed.
 
 (* Basic_1: was: pc3_pr2_u *)
 (* Basic_2A1: was: cpcs_cpr_strap2 *)
-lemma cpcs_cpr_step_sn (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+lemma cpcs_cpr_step_sn (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
 /3 width=3 by cpcs_step_sn, or_introl/ qed-.
 
 (* Basic_2A1: was: cpcs_cpr_strap1 *)
-lemma cpcs_cpr_step_dx (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+lemma cpcs_cpr_step_dx (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T →
+                                    ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
 /3 width=3 by cpcs_step_dx, or_introl/ qed-.
 
-lemma cpcs_cpr_div (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+lemma cpcs_cpr_div (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T →
+                                ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
 /3 width=3 by cpcs_step_dx, or_intror/ qed-.
 
-lemma cpr_div (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+lemma cpr_div (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T →
+                           ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
 /3 width=3 by cpr_cpcs_dx, cpcs_step_dx, or_intror/ qed-.
 
 (* Basic_1: was: pc3_pr2_u2 *)
-lemma cpcs_cpr_conf (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+lemma cpcs_cpr_conf (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T ➡[h] T1 →
+                                 ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
 /3 width=3 by cpcs_step_sn, or_intror/ qed-.
 
 (* Basic_1: removed theorems 9: