update in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / reqx_reqx.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma
index c43edbdd17c42112b483fc16072414a5a1adca2d..b6dc3d196b2cacee4373babb5767eca8164cac96 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma
@@ -12,21 +12,20 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/syntax/ext2_ext2.ma".
-include "static_2/syntax/teqx_teqx.ma".
-include "static_2/static/reqx_length.ma".
+include "static_2/static/reqg_reqg.ma".
+include "static_2/static/reqx.ma".
 
 (* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***)
 
 (* Advanced properties ******************************************************)
-
+(*
 lemma reqx_sym: ∀T. symmetric … (reqx T).
 /3 width=3 by reqx_fsge_comp, rex_sym, teqx_sym/ qed-.
-
+*)
 (* Basic_2A1: uses: lleq_dec *)
-lemma reqx_dec: â\88\80L1,L2. â\88\80T:term. Decidable (L1 â\89\9b[T] L2).
-/3 width=1 by rex_dec, teqx_dec/ qed-.
-
+lemma reqx_dec: â\88\80L1,L2. â\88\80T:term. Decidable (L1 â\89\85[T] L2).
+/2 width=1 by reqg_dec/ qed-.
+(*
 (* Main properties **********************************************************)
 
 (* Basic_2A1: uses: lleq_bind lleq_bind_O *)
@@ -60,9 +59,9 @@ theorem reqx_canc_sn: ∀T. left_cancellable … (reqx T).
 theorem reqx_canc_dx: ∀T. right_cancellable … (reqx T).
 /3 width=3 by reqx_trans, reqx_sym/ qed-.
 
-theorem reqx_repl: â\88\80L1,L2. â\88\80T:term. L1 â\89\9b[T] L2 →
-                   â\88\80K1. L1 â\89\9b[T] K1 â\86\92 â\88\80K2. L2 â\89\9b[T] K2 â\86\92 K1 â\89\9b[T] K2.
-/3 width=3 by reqx_canc_sn, reqx_trans/ qed-.
+theorem reqx_repl: â\88\80L1,L2. â\88\80T:term. L1 â\89\85[T] L2 →
+                   â\88\80K1. L1 â\89\85[T] K1 â\86\92 â\88\80K2. L2 â\89\85[T] K2 â\86\92 K1 â\89\85[T] K2.
+/2 width=5 by reqg_repl/ qed-.
 
 (* Negated properties *******************************************************)
 
@@ -96,3 +95,4 @@ lemma rneqx_inv_flat: ∀I,L1,L2,V,T. (L1 ≛[ⓕ[I]V.T] L2 → ⊥) →
 lemma rneqx_inv_bind_void: ∀p,I,L1,L2,V,T. (L1 ≛[ⓑ[p,I]V.T] L2 → ⊥) →
                            (L1 ≛[V] L2 → ⊥) ∨ (L1.ⓧ ≛[T] L2.ⓧ → ⊥).
 /3 width=3 by rnex_inv_bind_void, teqx_dec/ qed-.
+*)