- the relation for pointwise extensions now takes a binder as argument

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / lpr_lpr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
index 2f653c61bc6e9a9bb1689bf0b524410759095d23..d0b36345539e8b4415e950f93cc84c5108d2b851 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
@@ -26,7 +26,7 @@ fact cpr_conf_lpr_atom_atom:
 
 fact cpr_conf_lpr_atom_delta:
    ∀G,L0,i. (
-      â\88\80L,T. â¦\83G, L0, #iâ¦\84 â\8a\83+ ⦃G, L, T⦄ →
+      â\88\80L,T. â¦\83G, L0, #iâ¦\84 â\8a\90+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
@@ -50,7 +50,7 @@ qed-.
 (* Basic_1: includes: pr0_delta_delta pr2_delta_delta *)
 fact cpr_conf_lpr_delta_delta:
    ∀G,L0,i. (
-      â\88\80L,T. â¦\83G, L0, #iâ¦\84 â\8a\83+ ⦃G, L, T⦄ →
+      â\88\80L,T. â¦\83G, L0, #iâ¦\84 â\8a\90+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
@@ -77,7 +77,7 @@ qed-.
 
 fact cpr_conf_lpr_bind_bind:
    ∀a,I,G,L0,V0,T0. (
-      â\88\80L,T. â¦\83G, L0, â\93\91{a,I}V0.T0â¦\84 â\8a\83+ ⦃G, L, T⦄ →
+      â\88\80L,T. â¦\83G, L0, â\93\91{a,I}V0.T0â¦\84 â\8a\90+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
@@ -95,7 +95,7 @@ qed-.
 
 fact cpr_conf_lpr_bind_zeta:
    ∀G,L0,V0,T0. (
-      â\88\80L,T. â¦\83G, L0, +â\93\93V0.T0â¦\84 â\8a\83+ ⦃G, L, T⦄ →
+      â\88\80L,T. â¦\83G, L0, +â\93\93V0.T0â¦\84 â\8a\90+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
@@ -112,7 +112,7 @@ qed-.
 
 fact cpr_conf_lpr_zeta_zeta:
    ∀G,L0,V0,T0. (
-      â\88\80L,T. â¦\83G, L0, +â\93\93V0.T0â¦\84 â\8a\83+ ⦃G, L, T⦄ →
+      â\88\80L,T. â¦\83G, L0, +â\93\93V0.T0â¦\84 â\8a\90+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
@@ -131,7 +131,7 @@ qed-.
 
 fact cpr_conf_lpr_flat_flat:
    ∀I,G,L0,V0,T0. (
-      â\88\80L,T. â¦\83G, L0, â\93\95{I}V0.T0â¦\84 â\8a\83+ ⦃G, L, T⦄ →
+      â\88\80L,T. â¦\83G, L0, â\93\95{I}V0.T0â¦\84 â\8a\90+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
@@ -148,7 +148,7 @@ qed-.
 
 fact cpr_conf_lpr_flat_tau:
    ∀G,L0,V0,T0. (
-      â\88\80L,T. â¦\83G, L0, â\93\9dV0.T0â¦\84 â\8a\83+ ⦃G, L, T⦄ →
+      â\88\80L,T. â¦\83G, L0, â\93\9dV0.T0â¦\84 â\8a\90+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
@@ -163,7 +163,7 @@ qed-.
 
 fact cpr_conf_lpr_tau_tau:
    ∀G,L0,V0,T0. (
-      â\88\80L,T. â¦\83G, L0, â\93\9dV0.T0â¦\84 â\8a\83+ ⦃G, L, T⦄ →
+      â\88\80L,T. â¦\83G, L0, â\93\9dV0.T0â¦\84 â\8a\90+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
@@ -178,7 +178,7 @@ qed-.
 
 fact cpr_conf_lpr_flat_beta:
    ∀a,G,L0,V0,W0,T0. (
-      â\88\80L,T. â¦\83G, L0, â\93\90V0.â\93\9b{a}W0.T0â¦\84 â\8a\83+ ⦃G, L, T⦄ →
+      â\88\80L,T. â¦\83G, L0, â\93\90V0.â\93\9b{a}W0.T0â¦\84 â\8a\90+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
@@ -203,7 +203,7 @@ qed-.
 *)
 fact cpr_conf_lpr_flat_theta:
    ∀a,G,L0,V0,W0,T0. (
-      â\88\80L,T. â¦\83G, L0, â\93\90V0.â\93\93{a}W0.T0â¦\84 â\8a\83+ ⦃G, L, T⦄ →
+      â\88\80L,T. â¦\83G, L0, â\93\90V0.â\93\93{a}W0.T0â¦\84 â\8a\90+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
@@ -232,7 +232,7 @@ qed-.
 
 fact cpr_conf_lpr_beta_beta:
    ∀a,G,L0,V0,W0,T0. (
-      â\88\80L,T. â¦\83G, L0, â\93\90V0.â\93\9b{a}W0.T0â¦\84 â\8a\83+ ⦃G, L, T⦄ →
+      â\88\80L,T. â¦\83G, L0, â\93\90V0.â\93\9b{a}W0.T0â¦\84 â\8a\90+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
@@ -254,7 +254,7 @@ qed-.
 (* Basic_1: was: pr0_upsilon_upsilon *)
 fact cpr_conf_lpr_theta_theta:
    ∀a,G,L0,V0,W0,T0. (
-      â\88\80L,T. â¦\83G, L0, â\93\90V0.â\93\93{a}W0.T0â¦\84 â\8a\83+ ⦃G, L, T⦄ →
+      â\88\80L,T. â¦\83G, L0, â\93\90V0.â\93\93{a}W0.T0â¦\84 â\8a\90+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0