- cpxs_tsts_vector completed

- refactoring in etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpx/cpx_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpx/cpx_lreq.etc
new file mode 100644 (file)
index 0000000..9c41e25
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpx/cpx_lreq.etc
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/drop_lreq.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+
+(* Properties on equivalence for local environments *************************)
+
+lemma lreq_cpx_trans: ∀h,o,G. lsub_trans … (cpx h o G) (lreq 0 (∞)).
+#h #o #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
+[ //
+| /2 width=2 by cpx_st/
+| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
+  elim (lreq_drop_trans_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/
+|4,9: /4 width=1 by cpx_bind, cpx_beta, lreq_pair_O_Y/
+|5,7,8: /3 width=1 by cpx_flat, cpx_eps, cpx_ct/
+|6,10: /4 width=3 by cpx_zeta, cpx_theta, lreq_pair_O_Y/
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpx_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpx_lreq.ma
deleted file mode 100644 (file)
index 9c41e25..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpx_lreq.ma
+++ /dev/null
@@ -1,32 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/substitution/drop_lreq.ma".
-include "basic_2/reduction/cpx.ma".
-
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
-
-(* Properties on equivalence for local environments *************************)
-
-lemma lreq_cpx_trans: ∀h,o,G. lsub_trans … (cpx h o G) (lreq 0 (∞)).
-#h #o #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
-[ //
-| /2 width=2 by cpx_st/
-| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (lreq_drop_trans_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/
-|4,9: /4 width=1 by cpx_bind, cpx_beta, lreq_pair_O_Y/
-|5,7,8: /3 width=1 by cpx_flat, cpx_eps, cpx_ct/
-|6,10: /4 width=3 by cpx_zeta, cpx_theta, lreq_pair_O_Y/
-]
-qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpb/fpb_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpb/fpb_lift.etc
new file mode 100644 (file)
index 0000000..6fae399
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpb/fpb_lift.etc
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/unfold/lstas_da.ma".
+include "basic_2/reduction/cpx_lift.ma".
+include "basic_2/reduction/fpb.ma".
+
+(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************)
+
+(* Advanced properties ******************************************************)
+
+lemma sta_fpb: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 →
+               ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ ≻[h, o] ⦃G, L, T2⦄.
+#h #o #G #L #T1 #T2 #d #HT1 #HT12 elim (eq_term_dec T1 T2)
+/3 width=2 by fpb_cpx, sta_cpx/ #H destruct
+elim (lstas_inv_refl_pos h G L T2 0) //
+qed.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpb_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpb_lift.ma
deleted file mode 100644 (file)
index 6fae399..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpb_lift.ma
+++ /dev/null
@@ -1,28 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/unfold/lstas_da.ma".
-include "basic_2/reduction/cpx_lift.ma".
-include "basic_2/reduction/fpb.ma".
-
-(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************)
-
-(* Advanced properties ******************************************************)
-
-lemma sta_fpb: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 →
-               ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ ≻[h, o] ⦃G, L, T2⦄.
-#h #o #G #L #T1 #T2 #d #HT1 #HT12 elim (eq_term_dec T1 T2)
-/3 width=2 by fpb_cpx, sta_cpx/ #H destruct
-elim (lstas_inv_refl_pos h G L T2 0) //
-qed.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbq/fpbq_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbq/fpbq_lift.etc
new file mode 100644 (file)
index 0000000..4029d94
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbq/fpbq_lift.etc
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reduction/cpx_lift.ma".
+include "basic_2/reduction/fpbq.ma".
+
+(* "QRST" PARALLEL REDUCTION FOR CLOSURES ***********************************)
+
+(* Advanced properties ******************************************************)
+
+lemma sta_fpbq: ∀h,o,G,L,T1,T2,d.
+                 ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 → ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 →
+                 ⦃G, L, T1⦄ ≽[h, o] ⦃G, L, T2⦄.
+/3 width=4 by fpbq_cpx, sta_cpx/ qed.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbq_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbq_lift.ma
deleted file mode 100644 (file)
index 4029d94..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbq_lift.ma
+++ /dev/null
@@ -1,25 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/reduction/cpx_lift.ma".
-include "basic_2/reduction/fpbq.ma".
-
-(* "QRST" PARALLEL REDUCTION FOR CLOSURES ***********************************)
-
-(* Advanced properties ******************************************************)
-
-lemma sta_fpbq: ∀h,o,G,L,T1,T2,d.
-                 ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 → ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 →
-                 ⦃G, L, T1⦄ ≽[h, o] ⦃G, L, T2⦄.
-/3 width=4 by fpbq_cpx, sta_cpx/ qed.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/tsts/tsts.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tsts/tsts.etc
deleted file mode 100644 (file)
index 174cedd..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/tsts/tsts.etc
+++ /dev/null
@@ -1,11 +0,0 @@
-fact tsts_inv_pair2_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 →
-                         ∃∃W1,U1. T1 = ②{I}W1.U1.
-#T1 #T2 * -T1 -T2
-[ #J #I #W2 #U2 #H destruct
-| #J #V1 #V2 #T1 #T2 #I #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/
-]
-qed-.
-
-lemma tsts_inv_pair2: ∀I,T1,W2,U2. T1 ≂ ②{I}W2.U2 →
-                      ∃∃W1,U1. T1 = ②{I}W1.U1.
-/2 width=5 by tsts_inv_pair2_aux/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma
index 65c32bf7f9982d47d295bc87382bec46d807b2c7..e7d1e9ed9a3a55ed21aeeec776282028e8bde024 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma
@@ -30,20 +30,6 @@ lemma cpxs_fwd_sort: ∀h,o,G,L,U,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] U →
 ]
 qed-.
 
-(* Basic_1: was just: pr3_iso_beta *)
-lemma cpxs_fwd_beta: ∀h,o,p,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] U →
-                     ⓐV.ⓛ{p}W.T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] U.
-#h #o #p #G #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H *
-[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
-| #b #W0 #T0 #HT0 #HU
-  elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
-  lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1
-  /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/
-| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
-  elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
-]
-qed-.
-
 (* Note: probably this is an inversion lemma *)
 (* Basic_2A1: was: cpxs_fwd_delta *)
 lemma cpxs_fwd_delta_drops: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 →
@@ -58,6 +44,20 @@ elim (cpxs_lifts … HVU0 (Ⓣ) … L … HV12) -HVU0 -HV12 /2 width=3 by drops_
 <(lifts_mono … HU0 … H) -U0 -X /2 width=1 by or_intror/
 qed-.
 
+(* Basic_1: was just: pr3_iso_beta *)
+lemma cpxs_fwd_beta: ∀h,o,p,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] U →
+                     ⓐV.ⓛ{p}W.T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] U.
+#h #o #p #G #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H *
+[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
+| #b #W0 #T0 #HT0 #HU
+  elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
+  lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1
+  /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/
+| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
+  elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
+]
+qed-.
+
 lemma cpxs_fwd_theta: ∀h,o,p,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] U →
                       ∀V2. ⬆*[1] V1 ≡ V2 → ⓐV1.ⓓ{p}V.T ⩳[h, o] U ∨
                       ⦃G, L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] U.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts_vector.ma
index 6252ed90eae75ba248f860f05d52a673e2745c49..cf7cdba9dfff71838ce09bb16eb83108aad76f44 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts_vector.ma
@@ -12,109 +12,93 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/syntax/tsts_vector.ma".
-include "basic_2/substitution/lift_vector.ma".
-include "basic_2/computation/cpxs_tsts.ma".
+include "basic_2/syntax/tsts_simple_vector.ma".
+include "basic_2/relocation/lifts_vector.ma".
+include "basic_2/rt_computation/cpxs_tsts.ma".
 
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
 
-(* Vector form of forward lemmas involving same top term structure **********)
+(* Vector form of forward lemmas with same top term structure ***************)
 
-(* Basic_1: was just: nf2_iso_appls_lref *)
-lemma cpxs_fwd_cnx_vector: ∀h,o,G,L,T.  𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ →
-                           ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ⬈*[h, o] U → ⒶVs.T ≂ U.
-#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
-#V #Vs #IHVs #U #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair/
-| #a #W0 #T0 #HT0 #HU
-  lapply (IHVs … HT0) -IHVs -HT0 #HT0
-  elim (tsts_inv_bind_applv_simple … HT0) //
-| #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
-  lapply (IHVs … HT0) -IHVs -HT0 #HT0
-  elim (tsts_inv_bind_applv_simple … HT0) //
-]
-qed-.
-
-lemma cpxs_fwd_sort_vector: ∀h,o,G,L,s,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆s ⬈*[h, o] U →
-                            ⒶVs.⋆s ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.⋆(next h s) ⬈*[h, o] U.
+lemma cpxs_fwd_sort_vector: ∀h,o,G,L,s,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆s ⬈*[h] U →
+                            ⒶVs.⋆s ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.⋆(next h s) ⬈*[h] U.
 #h #o #G #L #s #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/
 #V #Vs #IHVs #U #H
 elim (cpxs_inv_appl1 … H) -H *
 [ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
-| #a #W1 #T1 #HT1 #HU
+| #p #W1 #T1 #HT1 #HU
   elim (IHVs … HT1) -IHVs -HT1 #HT1
-  [ elim (tsts_inv_bind_applv_simple … HT1) //
+  [ elim (tsts_inv_applv_bind_simple … HT1) //
   | @or_intror (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
-    @(cpxs_strap1 … (ⓐV.ⓛ{a}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
+    @(cpxs_strap1 … (ⓐV.ⓛ{p}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/
   ]
-| #a #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
+| #p #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
   elim (IHVs … HT1) -IHVs -HT1 #HT1
-  [ elim (tsts_inv_bind_applv_simple … HT1) //
+  [ elim (tsts_inv_applv_bind_simple … HT1) //
   | @or_intror (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
-    @(cpxs_strap1 … (ⓐV1.ⓓ{a}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
+    @(cpxs_strap1 … (ⓐV1.ⓓ{p}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/
   ]
 ]
 qed-.
 
-
-(* Basic_1: was just: pr3_iso_appls_beta *)
-lemma cpxs_fwd_beta_vector: ∀h,o,a,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ⬈*[h, o] U →
-                            ⒶVs. ⓐV. ⓛ{a}W. T ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{a}ⓝW.V.T ⬈*[h, o] U.
-#h #o #a #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
-#V0 #Vs #IHVs #V #W #T #U #H
+(* Basic_2A1: was: cpxs_fwd_delta_vector *)
+lemma cpxs_fwd_delta_drops_vector: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 →
+                                   ∀V2. ⬆*[⫯i] V1 ≡ V2 →
+                                   ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.#i ⬈*[h] U →
+                                   ⒶVs.#i ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.V2 ⬈*[h] U.
+#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta_drops/
+#V #Vs #IHVs #U #H -K -V1
 elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
-| #b #W1 #T1 #HT1 #HU
-  elim (IHVs … HT1) -IHVs -HT1 #HT1
-  [ elim (tsts_inv_bind_applv_simple … HT1) //
-  | @or_intror (**) (* explicit constructor *)
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
+| #q #W0 #T0 #HT0 #HU
+  elim (IHVs … HT0) -IHVs -HT0 #HT0
+  [ elim (tsts_inv_applv_bind_simple … HT0) //
+  | @or_intror -i (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
-    @(cpxs_strap1 … (ⓐV0.ⓛ{b}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
+    @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /3 width=1 by cpxs_flat_dx, cpx_beta/
   ]
-| #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
-  elim (IHVs … HT1) -IHVs -HT1 #HT1
-  [ elim (tsts_inv_bind_applv_simple … HT1) //
-  | @or_intror (**) (* explicit constructor *)
+| #q #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
+  elim (IHVs … HT0) -IHVs -HT0 #HT0
+  [ elim (tsts_inv_applv_bind_simple … HT0) //
+  | @or_intror -i (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
-    @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
+    @(cpxs_strap1 … (ⓐV0.ⓓ{q}V3.T0)) /3 width=3 by cpxs_flat, cpx_theta/
   ]
 ]
 qed-.
 
-lemma cpxs_fwd_delta_vector: ∀h,o,I,G,L,K,V1,i. ⬇[i] L ≡ K.ⓑ{I}V1 →
-                             ∀V2. ⬆[0, i + 1] V1 ≡ V2 →
-                             ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.#i ⬈*[h, o] U →
-                             ⒶVs.#i ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.V2 ⬈*[h, o] U.
-#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta/
-#V #Vs #IHVs #U #H -K -V1
+(* Basic_1: was just: pr3_iso_appls_beta *)
+lemma cpxs_fwd_beta_vector: ∀h,o,p,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{p}W.T ⬈*[h] U →
+                            ⒶVs.ⓐV.ⓛ{p}W. T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{p}ⓝW.V.T ⬈*[h] U.
+#h #o #p #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
+#V0 #Vs #IHVs #V #W #T #U #H
 elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
-| #b #W0 #T0 #HT0 #HU
-  elim (IHVs … HT0) -IHVs -HT0 #HT0
-  [ elim (tsts_inv_bind_applv_simple … HT0) //
-  | @or_intror -i (**) (* explicit constructor *)
+[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
+| #q #W1 #T1 #HT1 #HU
+  elim (IHVs … HT1) -IHVs -HT1 #HT1
+  [ elim (tsts_inv_applv_bind_simple … HT1) //
+  | @or_intror (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
-    @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
+    @(cpxs_strap1 … (ⓐV0.ⓛ{q}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/
   ]
-| #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
-  elim (IHVs … HT0) -IHVs -HT0 #HT0
-  [ elim (tsts_inv_bind_applv_simple … HT0) //
-  | @or_intror -i (**) (* explicit constructor *)
+| #q #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
+  elim (IHVs … HT1) -IHVs -HT1 #HT1
+  [ elim (tsts_inv_applv_bind_simple … HT1) //
+  | @or_intror (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
-    @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
+    @(cpxs_strap1 … (ⓐV1.ⓓ{q}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/
   ]
 ]
 qed-.
 
 (* Basic_1: was just: pr3_iso_appls_abbr *)
-lemma cpxs_fwd_theta_vector: ∀h,o,G,L,V1b,V2b. ⬆[0, 1] V1b ≡ V2b →
-                             ∀a,V,T,U. ⦃G, L⦄ ⊢ ⒶV1b.ⓓ{a}V.T ⬈*[h, o] U →
-                             ⒶV1b. ⓓ{a}V. T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}V.ⒶV2b.T ⬈*[h, o] U.
+lemma cpxs_fwd_theta_vector: ∀h,o,G,L,V1b,V2b. ⬆*[1] V1b ≡ V2b →
+                             ∀p,V,T,U. ⦃G, L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] U →
+                             ⒶV1b.ⓓ{p}V.T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] U.
 #h #o #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/
-#V1b #V2b #V1a #V2a #HV12a #HV12b #a
+#V1b #V2b #V1a #V2a #HV12a #HV12b #p
 generalize in match HV12a; -HV12a
 generalize in match V2a; -V2a
 generalize in match V1a; -V1a
@@ -122,22 +106,22 @@ elim HV12b -V1b -V2b /2 width=1 by cpxs_fwd_theta/
 #V1b #V2b #V1b #V2b #HV12b #_ #IHV12b #V1a #V2a #HV12a #V #T #U #H
 elim (cpxs_inv_appl1 … H) -H *
 [ -IHV12b -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
-| #b #W0 #T0 #HT0 #HU
+| #q #W0 #T0 #HT0 #HU
   elim (IHV12b … HV12b … HT0) -IHV12b -HT0 #HT0
   [ -HV12a -HV12b -HU
     elim (tsts_inv_pair1 … HT0) #V1 #T1 #H destruct
   | @or_intror -V1b (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
     elim (cpxs_inv_abbr1 … HT0) -HT0 *
-    [ -HV12a -HV12b #V1 #T1 #_ #_ #H destruct
+    [ -HV12a #V1 #T1 #_ #_ #H destruct
     | -V1b #X #HT1 #H #H0 destruct
-      elim (lift_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
-      @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{b}W1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b
-      @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0))
-      /4 width=7 by cpxs_beta_dx, cpx_zeta, lift_bind, lift_flat/
+      elim (lifts_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
+      @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{q}W1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b
+      @(cpxs_strap2 … (ⓐV1a.ⓛ{q}W0.T0))
+      /4 width=7 by cpxs_beta_dx, cpx_zeta, lifts_bind, lifts_flat/
     ]
   ]
-| #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU
+| #q #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU
   elim (IHV12b … HV12b … HT0) -HV12b -IHV12b -HT0 #HT0
   [ -HV12a -HV10a -HV0a -HU
     elim (tsts_inv_pair1 … HT0) #V1 #T1 #H destruct
@@ -145,46 +129,64 @@ elim (cpxs_inv_appl1 … H) -H *
     @(cpxs_trans … HU) -U
     elim (cpxs_inv_abbr1 … HT0) -HT0 *
     [ #V1 #T1 #HV1 #HT1 #H destruct
-      lapply (cpxs_lift … HV10a (L.ⓓV) (Ⓕ) … HV12a … HV0a) -V1a -V0a [ /2 width=1 by drop_drop/ ] #HV2a
-      @(cpxs_trans … (ⓓ{a}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/
+      elim (cpxs_lifts … HV10a (Ⓣ) … (L.ⓓV) … HV12a) -V1a /3 width=1 by drops_refl, drops_drop/ #X #H
+      <(lifts_mono … HV0a … H) -V0a -X #HV2a
+      @(cpxs_trans … (ⓓ{p}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/
     | #X #HT1 #H #H0 destruct
-      elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
-      lapply (cpxs_lift … HV10a (L.ⓓV0) (Ⓕ) … HV12a … HV0a) -V0a [ /2 width=1 by drop_drop/ ] #HV2a
-      @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b
-      @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V1 -T1
-      @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/
+      elim (lifts_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
+      elim (cpxs_lifts … HV10a (Ⓣ) … (L.ⓓV0) … HV12a) /3 width=1 by drops_refl, drops_drop/ #X #H
+      <(lifts_mono … HV0a … H) -V0a -X #HV2a
+      @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{q}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b
+      @(cpxs_strap2 … (ⓐV1a.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V1 -T1
+      @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/
     ]
   ]
 ]
 qed-.
 
 (* Basic_1: was just: pr3_iso_appls_cast *)
-lemma cpxs_fwd_cast_vector: ∀h,o,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ⬈*[h, o] U →
-                            â\88¨â\88¨ â\92¶Vs. â\93\9dW. T â\89\82 U
-                             | ⦃G, L⦄ ⊢ ⒶVs.T ⬈*[h, o] U
-                             | ⦃G, L⦄ ⊢ ⒶVs.W ⬈*[h, o] U.
+lemma cpxs_fwd_cast_vector: ∀h,o,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ⬈*[h] U →
+                            â\88¨â\88¨ â\92¶Vs. â\93\9dW. T ⩳[h, o] U
+                             | ⦃G, L⦄ ⊢ ⒶVs.T ⬈*[h] U
+                             | ⦃G, L⦄ ⊢ ⒶVs.W ⬈*[h] U.
 #h #o #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
 #V #Vs #IHVs #W #T #U #H
 elim (cpxs_inv_appl1 … H) -H *
 [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/
-| #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0
-  [ elim (tsts_inv_bind_applv_simple … HT0) //
+| #q #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0
+  [ elim (tsts_inv_applv_bind_simple … HT0) //
   | @or3_intro1 -W (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
-    @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
+    @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
   | @or3_intro2 -T (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
-    @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
+    @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
   ]
-| #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
+| #q #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
   elim (IHVs … HT0) -IHVs -HT0 #HT0
-  [ elim (tsts_inv_bind_applv_simple … HT0) //
+  [ elim (tsts_inv_applv_bind_simple … HT0) //
   | @or3_intro1 -W (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
-    @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
+    @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
   | @or3_intro2 -T (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
-    @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
+    @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
   ]
 ]
 qed-.
+
+(* Basic_1: was just: nf2_iso_appls_lref *)
+lemma cpxs_fwd_cnx_vector: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ →
+                           ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ⬈*[h] U → ⒶVs.T ⩳[h, o] U.
+#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
+#V #Vs #IHVs #U #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair/
+| #p #W0 #T0 #HT0 #HU
+  lapply (IHVs … HT0) -IHVs -HT0 #HT0
+  elim (tsts_inv_applv_bind_simple … HT0) //
+| #p #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
+  lapply (IHVs … HT0) -IHVs -HT0 #HT0
+  elim (tsts_inv_applv_bind_simple … HT0) //
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
index 57e4223680164fa8b6ac9e3034372127c8319e6a..68c8d4eac4642f19ea914b462e2f40e182713f81 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
@@ -1,4 +1,4 @@
-cpxs.ma cpxs_tdeq.ma cpxs_tsts.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
+cpxs.ma cpxs_tdeq.ma cpxs_tsts.ma cpxs_tsts_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
 lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma
 csx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma
 csx_vector.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma
index d489fca883b6910b39aa3ab94bfbce6f83468c16..6ea5dc782359ead4bacdcfde9c721aedf83fb524 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma
@@ -67,8 +67,8 @@ lemma tsts_inv_gref1: ∀h,o,Y,l. §l ⩳[h, o] Y → Y = §l.
 /2 width=5 by tsts_inv_gref1_aux/ qed-.
 
 fact tsts_inv_pair1_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 →
-                         ∀I,W1,U1. T1 = ②{I}W1.U1 →
-                         ∃∃W2,U2. T2 = ②{I}W2.U2.
+                         ∀J,W1,U1. T1 = ②{J}W1.U1 →
+                         ∃∃W2,U2. T2 = ②{J}W2.U2.
 #h #o #T1 #T2 * -T1 -T2
 [ #s1 #s2 #d #_ #_ #J #W1 #U1 #H destruct
 | #i #J #W1 #U1 #H destruct
@@ -82,6 +82,21 @@ lemma tsts_inv_pair1: ∀h,o,J,W1,U1,T2. ②{J}W1.U1 ⩳[h, o] T2 →
                       ∃∃W2,U2. T2 = ②{J}W2. U2.
 /2 width=7 by tsts_inv_pair1_aux/ qed-.
 
+fact tsts_inv_pair2_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 →
+                         ∀J,W2,U2. T2 = ②{J}W2.U2 →
+                         ∃∃W1,U1. T1 = ②{J}W1.U1.
+#h #o #T1 #T2 * -T1 -T2
+[ #s1 #s2 #d #_ #_ #J #W2 #U2 #H destruct
+| #i #J #W2 #U2 #H destruct
+| #l #J #W2 #U2 #H destruct
+| #I #V1 #V2 #T1 #T2 #J #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/
+]
+qed-.
+
+lemma tsts_inv_pair2: ∀h,o,J,T1,W2,U2. T1 ⩳[h, o] ②{J}W2.U2 →
+                      ∃∃W1,U1. T1 = ②{J}W1.U1.
+/2 width=7 by tsts_inv_pair2_aux/ qed-.
+
 (* Advanced inversion lemmas ************************************************)
 
 lemma tsts_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → ∀d. deg h o s1 d →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple_vector.ma
new file mode 100644 (file)
index 0000000..2320a0c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple_vector.ma
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/syntax/term_vector.ma".
+include "basic_2/syntax/tsts_simple.ma".
+
+(* SAME TOP TERM STRUCTURE **************************************************)
+
+(* Advanced inversion lemmas with simple (neutral) terms ********************)
+
+(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
+(* Basic_2A1: was: tsts_inv_bind_applv_simple *)
+lemma tsts_inv_applv_bind_simple: ∀h,o,p,I,Vs,V2,T1,T2. ⒶVs.T1 ⩳[h, o] ⓑ{p,I}V2.T2 →
+                                  𝐒⦃T1⦄ → ⊥.
+#h #o #p #I #Vs #V2 #T1 #T2 #H elim (tsts_inv_pair2 … H) -H
+#V0 #T0 elim Vs -Vs normalize
+[ #H destruct #H /2 width=5 by simple_inv_bind/
+| #V #Vs #_ #H destruct
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_vector.ma
deleted file mode 100644 (file)
index aba7469..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_vector.ma
+++ /dev/null
@@ -1,32 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/syntax/term_vector.ma".
-include "basic_2/syntax/tsts_simple.ma".
-
-(* SAME TOP TERM STRUCTURE **************************************************)
-
-(* Advanced inversion lemmas with simple (neutral) terms ********************)
-(*
-(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
-(* Basic_2A1: was: tsts_inv_bind_applv_simple *)
-lemma tsts_inv_applv_bind_simple: ∀h,o,p,I,Vs,V2,T1,T2. ⒶVs.T1 ⩳[h, o] ⓑ{p,I}V2.T2 →
-                                  𝐒⦃T1⦄ → ⊥.
-#h #o #p #I #Vs #V2 #T1 #T2 #H elim (tsts_inv_pair2 … H) -H
-#V0 #T0 elim Vs -Vs normalize
-[ #H destruct #H /2 width=5 by simple_inv_bind/
-| #V #Vs #_ #H destruct
-]
-qed-.
-*)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 305dbb057f44e943ac19d7c9b8d5295692b8f5d9..22f988e72a5b56f3970be3a84ec5a75deb078164 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -241,7 +241,7 @@ table {
           }
         ]
         [ { "same top term structure" * } {
-             [ "tsts ( ? ⩳[?,?] ? )" "tsts_simple" + "tsts_tdeq" + "tsts_tsts" + "tsts_vector" * ]
+             [ "tsts ( ? ⩳[?,?] ? )" "tsts_simple" + "tsts_tdeq" + "tsts_tsts" + "tsts_simple_vector" * ]
           }
         ]
         [ { "degree-based equivalence for terms" * } {