X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Freq.ma;h=93aaafbb476cce6360568ec5ef210f98357bcb23;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hp=fcd79b33a68ddf9c8068ef631fe95d0da61993e4;hpb=bd53c4e895203eb049e75434f638f26b5a161a2b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/req.ma b/matita/matita/contribs/lambdadelta/static_2/static/req.ma
index fcd79b33a..93aaafbb4 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/req.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/req.ma
@@ -13,91 +13,86 @@
 (**************************************************************************)
 
 include "static_2/notation/relations/ideqsn_3.ma".
-include "static_2/static/rex.ma".
+include "static_2/syntax/teq_ext.ma".
+include "static_2/static/reqg.ma".
 
 (* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
 
 (* Basic_2A1: was: lleq *)
 definition req: relation3 term lenv lenv ≝
-                rex ceq.
+           reqg (pr_eq …).
 
 interpretation
-   "syntactic equivalence on referred entries (local environment)"
-   'IdEqSn T L1 L2 = (req T L1 L2).
+  "syntactic equivalence on referred entries (local environment)"
+  'IdEqSn T L1 L2 = (req T L1 L2).
 
-(* Note: "req_transitive R" is equivalent to "rex_transitive ceq R R" *)
+(* Note: "R_transitive_req R" is equivalent to "R_transitive_rex ceq R R" *)
 (* Basic_2A1: uses: lleq_transitive *)
-definition req_transitive: predicate (relation3 lenv term term) ≝
+definition R_transitive_req: predicate (relation3 lenv term term) ≝
            λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1] L2 → R L1 T1 T2.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma req_inv_bind: ∀p,I,L1,L2,V,T. L1 ≡[ⓑ[p,I]V.T] L2 →
-                    ∧∧ L1 ≡[V] L2 & L1.ⓑ[I]V ≡[T] L2.ⓑ[I]V.
-/2 width=2 by rex_inv_bind/ qed-.
+lemma req_inv_bind:
+      ∀p,I,L1,L2,V,T. L1 ≡[ⓑ[p,I]V.T] L2 →
+      ∧∧ L1 ≡[V] L2 & L1.ⓑ[I]V ≡[T] L2.ⓑ[I]V.
+/2 width=2 by reqg_inv_bind_refl/ qed-.
 
-lemma req_inv_flat: ∀I,L1,L2,V,T. L1 ≡[ⓕ[I]V.T] L2 →
-                    ∧∧ L1 ≡[V] L2 & L1 ≡[T] L2.
-/2 width=2 by rex_inv_flat/ qed-.
+lemma req_inv_flat:
+      ∀I,L1,L2,V,T. L1 ≡[ⓕ[I]V.T] L2 →
+      ∧∧ L1 ≡[V] L2 & L1 ≡[T] L2.
+/2 width=2 by reqg_inv_flat/ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma req_inv_zero_pair_sn: ∀I,L2,K1,V. K1.ⓑ[I]V ≡[#0] L2 →
-                            ∃∃K2. K1 ≡[V] K2 & L2 = K2.ⓑ[I]V.
+lemma req_inv_zero_pair_sn:
+      ∀I,L2,K1,V. K1.ⓑ[I]V ≡[#0] L2 →
+      ∃∃K2. K1 ≡[V] K2 & L2 = K2.ⓑ[I]V.
 #I #L2 #K1 #V #H
-elim (rex_inv_zero_pair_sn … H) -H #K2 #X #HK12 #HX #H destruct
-/2 width=3 by ex2_intro/
+elim (reqg_inv_zero_pair_sn … H) -H #K2 #X #HK12 #HX #H destruct
+@(teq_repl_1 … HX) -X
+@(ex2_intro … HK12) // (**) (* auto fails because a δ-expamsion gets in the way *)
 qed-.
 
-lemma req_inv_zero_pair_dx: ∀I,L1,K2,V. L1 ≡[#0] K2.ⓑ[I]V →
-                            ∃∃K1. K1 ≡[V] K2 & L1 = K1.ⓑ[I]V.
+lemma req_inv_zero_pair_dx:
+      ∀I,L1,K2,V. L1 ≡[#0] K2.ⓑ[I]V →
+      ∃∃K1. K1 ≡[V] K2 & L1 = K1.ⓑ[I]V.
 #I #L1 #K2 #V #H
-elim (rex_inv_zero_pair_dx … H) -H #K1 #X #HK12 #HX #H destruct
-/2 width=3 by ex2_intro/
+elim (reqg_inv_zero_pair_dx … H) -H #K1 #X #HK12 #HX #H destruct
+@(teq_repl_1 … HX) -V
+@(ex2_intro … HK12) // (**) (* auto fails because a δ-expamsion gets in the way *)
 qed-.
 
-lemma req_inv_lref_bind_sn: ∀I1,K1,L2,i. K1.ⓘ[I1] ≡[#↑i] L2 →
-                            ∃∃I2,K2. K1 ≡[#i] K2 & L2 = K2.ⓘ[I2].
-/2 width=2 by rex_inv_lref_bind_sn/ qed-.
+lemma req_inv_lref_bind_sn:
+      ∀I1,K1,L2,i. K1.ⓘ[I1] ≡[#↑i] L2 →
+      ∃∃I2,K2. K1 ≡[#i] K2 & L2 = K2.ⓘ[I2].
+/2 width=2 by reqg_inv_lref_bind_sn/ qed-.
 
-lemma req_inv_lref_bind_dx: ∀I2,K2,L1,i. L1 ≡[#↑i] K2.ⓘ[I2] →
-                            ∃∃I1,K1. K1 ≡[#i] K2 & L1 = K1.ⓘ[I1].
-/2 width=2 by rex_inv_lref_bind_dx/ qed-.
+lemma req_inv_lref_bind_dx:
+      ∀I2,K2,L1,i. L1 ≡[#↑i] K2.ⓘ[I2] →
+      ∃∃I1,K1. K1 ≡[#i] K2 & L1 = K1.ⓘ[I1].
+/2 width=2 by reqg_inv_lref_bind_dx/ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 (* Basic_2A1: was: llpx_sn_lrefl *)
 (* Basic_2A1: this should have been lleq_fwd_llpx_sn *)
-lemma req_fwd_rex: ∀R. c_reflexive … R →
-                   ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤[R,T] L2.
+lemma req_fwd_rex (R):
+      c_reflexive … R →
+      ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤[R,T] L2.
 #R #HR #L1 #L2 #T * #f #Hf #HL12
-/4 width=7 by sex_co, cext2_co, ex2_intro/
+/5 width=7 by sex_co, cext2_co, teq_repl_1, ex2_intro/
 qed-.
 
-(* Basic_properties *********************************************************)
-
-lemma frees_req_conf: ∀f,L1,T. L1 ⊢ 𝐅+❪T❫ ≘ f →
-                      ∀L2. L1 ≡[T] L2 → L2 ⊢ 𝐅+❪T❫ ≘ f.
-#f #L1 #T #H elim H -f -L1 -T
-[ /2 width=3 by frees_sort/
-| #f #i #Hf #L2 #H2
-  >(rex_inv_atom_sn … H2) -L2
-  /2 width=1 by frees_atom/
-| #f #I #L1 #V1 #_ #IH #Y #H2
-  elim (req_inv_zero_pair_sn … H2) -H2 #L2 #HL12 #H destruct
-  /3 width=1 by frees_pair/
-| #f #I #L1 #Hf #Y #H2
-  elim (rex_inv_zero_unit_sn … H2) -H2 #g #L2 #_ #_ #H destruct
-  /2 width=1 by frees_unit/
-| #f #I #L1 #i #_ #IH #Y #H2
-  elim (req_inv_lref_bind_sn … H2) -H2 #J #L2 #HL12 #H destruct
-  /3 width=1 by frees_lref/
-| /2 width=1 by frees_gref/
-| #f1V #f1T #f1 #p #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #L2 #H2
-  elim (req_inv_bind … H2) -H2 /3 width=5 by frees_bind/
-| #f1V #f1T #f1 #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #L2 #H2
-  elim (req_inv_flat … H2) -H2 /3 width=5 by frees_flat/
-]
+lemma req_fwd_reqg (S) (T:term):
+      reflexive … S →
+      ∀L1,L2. L1 ≡[T] L2 → L1 ≛[S,T] L2.
+/3 width=1 by req_fwd_rex, teqg_refl/ qed-.
+
+lemma transitive_req_fwd_rex (R):
+      R_transitive_req R → R_transitive_rex ceq R R.
+#R #HR #L1 #L #T1 #HL1 #T #HT #T2 #HT2
+@(HR … HL1) -HR -HL1 >(teq_inv_eq … HT) -T1 // (**)
 qed-.
 
 (* Basic_2A1: removed theorems 10: