From 7ad8c044ab33ea0f2aebb1c40fa20340d7f2f3eb Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 12 Oct 2013 17:38:16 +0000
Subject: [PATCH] some renaming ...

---
 .../basic_2/computation/cpxs_lift.ma          |  58 +++++-----
 .../lambdadelta/basic_2/computation/fpbg.ma   |   8 +-
 .../lambdadelta/basic_2/computation/fpbs.ma   |  10 +-
 .../basic_2/computation/fpbs_alt.ma           |   8 +-
 .../basic_2/computation/lpxs_cpxs.ma          |  36 +++----
 .../lambdadelta/basic_2/dynamic/snv_da_lpr.ma |  30 +++---
 .../lambdadelta/basic_2/dynamic/snv_lift.ma   |   4 +-
 .../lambdadelta/basic_2/dynamic/snv_lpr.ma    |  66 ++++++------
 .../lambdadelta/basic_2/dynamic/snv_lsstas.ma |  12 +--
 .../basic_2/dynamic/snv_lsstas_lpr.ma         |  48 ++++-----
 .../lambdadelta/basic_2/equivalence/cpcs.ma   |   2 +-
 .../contribs/lambdadelta/basic_2/names.txt    |   1 +
 .../lambdadelta/basic_2/reduction/cpx_lift.ma |  44 ++++----
 .../lambdadelta/basic_2/reduction/fpb.ma      |   8 +-
 .../lambdadelta/basic_2/reduction/fpbc.ma     |  20 ++--
 .../basic_2/reduction/lpr_ldrop.ma            |  22 ++--
 .../lambdadelta/basic_2/reduction/lpr_lpr.ma  |   8 +-
 .../basic_2/reduction/lpx_ldrop.ma            |  44 ++++----
 .../basic_2/relocation/{fsup.ma => fqu.ma}    |  36 +++----
 .../basic_2/relocation/{fsupq.ma => fquq.ma}  |  36 +++----
 .../relocation/{fsupq_alt.ma => fquq_alt.ma}  |  30 +++---
 .../lambdadelta/basic_2/substitution/fqup.ma  | 102 ++++++++++++++++++
 .../{fsupp_fsupp.ma => fqup_fqup.ma}          |   4 +-
 .../lambdadelta/basic_2/substitution/fqus.ma  |  69 ++++++++++++
 .../{fsups_fsups.ma => fqus_fqus.ma}          |   4 +-
 .../lambdadelta/basic_2/substitution/fsupp.ma | 102 ------------------
 .../lambdadelta/basic_2/substitution/fsups.ma |  69 ------------
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |   6 +-
 28 files changed, 444 insertions(+), 443 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/relocation/{fsup.ma => fqu.ma} (60%)
 rename matita/matita/contribs/lambdadelta/basic_2/relocation/{fsupq.ma => fquq.ma} (61%)
 rename matita/matita/contribs/lambdadelta/basic_2/relocation/{fsupq_alt.ma => fquq_alt.ma} (61%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma
 rename matita/matita/contribs/lambdadelta/basic_2/substitution/{fsupp_fsupp.ma => fqup_fqup.ma} (93%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma
 rename matita/matita/contribs/lambdadelta/basic_2/substitution/{fsups_fsups.ma => fqus_fqus.ma} (93%)
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
index 182043d3b..8028270d6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/fsups_fsups.ma".
+include "basic_2/substitution/fqus_fqus.ma".
 include "basic_2/unfold/lsstas_lift.ma".
 include "basic_2/reduction/cpx_lift.ma".
 include "basic_2/computation/cpxs.ma".
@@ -71,47 +71,47 @@ qed-.
 
 (* Properties on supclosure *************************************************)
 
-lemma fsupq_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 →
-                        ∀T1. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                        ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+lemma fquq_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 →
+                       ∀T1. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
 #h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2
-[ /3 width=3 by fsupq_fsups, ex2_intro/
+[ /3 width=3 by fquq_fqus, ex2_intro/
 | #T #T2 #HT2 #_ #IHTU2 #T1 #HT1
-  elim (fsupq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2
+  elim (fquq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2
   elim (IHTU2 … HT2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/
 ]
 qed-.
 
-lemma fsupq_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                          ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 →
-                          ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 →
-                          ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-/3 width=5 by fsupq_cpxs_trans, lsstas_cpxs/ qed-.
+lemma fquq_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                         ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 →
+                         ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 →
+                         ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+/3 width=5 by fquq_cpxs_trans, lsstas_cpxs/ qed-.
 
-lemma fsups_cpxs_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
-                        ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 →
-                        ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2
+lemma fqus_cpxs_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                       ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 →
+                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2
 [ /2 width=3 by ex2_intro/
 | #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
-  elim (fsupq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2
-  elim (IHT1 … HT2) -T /3 width=7 by fsups_trans, ex2_intro/
+  elim (fquq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2
+  elim (IHT1 … HT2) -T /3 width=7 by fqus_trans, ex2_intro/
 ]
 qed-.
 
-lemma fsups_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
-                          ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 →
-                          ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 →
-                          ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-/3 width=7 by fsups_cpxs_trans, lsstas_cpxs/ qed-.
+lemma fqus_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                         ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 →
+                         ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 →
+                         ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+/3 width=7 by fqus_cpxs_trans, lsstas_cpxs/ qed-.
 
-lemma fsups_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
-                       ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
-                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2
+lemma fqus_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                      ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
+                      ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2
 [ /2 width=3 by ex2_intro/
 | #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
-  elim (fsupq_cpx_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2
-  elim (IHT1 … HT2) -T /3 width=7 by fsups_strap1, ex2_intro/
+  elim (fquq_cpx_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2
+  elim (IHT1 … HT2) -T /3 width=7 by fqus_strap1, ex2_intro/
 ]
-qed-.
\ No newline at end of file
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
index 5a7e77736..f400f5c43 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/btpredstarproper_8.ma".
-include "basic_2/substitution/fsupp.ma".
+include "basic_2/substitution/fqup.ma".
 include "basic_2/reduction/fpbc.ma".
 include "basic_2/computation/fpbs.ma".
 
@@ -68,9 +68,9 @@ lemma fpbs_fpbg_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L
 /3 width=5 by fpbg_strap2/
 qed-.
 
-lemma fsupp_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2
-/4 width=5 by fpbg_strap1, fpbc_fpbg, fpbc_fsup, fpb_fsupq, fsup_fsupq/
+lemma fqup_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … L2 T2 H) -G2 -L2 -T2
+/4 width=5 by fpbg_strap1, fpbc_fpbg, fpbc_fqu, fpb_fquq, fqu_fquq/
 qed.
 
 lemma cpxs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
index 00f4a93aa..8d42f50bf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/btpredstar_8.ma".
-include "basic_2/substitution/fsups.ma".
+include "basic_2/substitution/fqus.ma".
 include "basic_2/reduction/fpb.ma".
 include "basic_2/computation/cpxs.ma".
 include "basic_2/computation/lpxs.ma".
@@ -55,10 +55,10 @@ lemma fpbs_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] 
                    ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
 /2 width=5 by tri_TC_strap/ qed-.
 
-lemma fsups_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
-                  ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … L2 T2 H) -G2 -L2 -T2 
-/3 width=5 by fpb_fsupq, tri_step/
+lemma fqus_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                 ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … L2 T2 H) -G2 -L2 -T2 
+/3 width=5 by fpb_fquq, tri_step/
 qed.
 
 lemma cpxs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
index 1b0471ddb..9e5336c04 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
@@ -34,11 +34,11 @@ lemma fpb_fpbsa_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L
                        ∀G2,L2,T2. ⦃G, L, T⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄.
 #h #g #G1 #G #L1 #L #T1 #T * -G -L -T [ #G #L #T #HG1 | #T #HT1 | #L #HL1 ]   
 #G2 #L2 #T2 * #L0 #T0 #HT0 #HG2 #HL02
-[ elim (fsupq_cpxs_trans … HT0 … HG1) -T
-  /3 width=7 by fsups_trans, ex3_2_intro/
+[ elim (fquq_cpxs_trans … HT0 … HG1) -T
+  /3 width=7 by fqus_trans, ex3_2_intro/
 | /3 width=5 by cpxs_strap2, ex3_2_intro/
 | lapply (lpx_cpxs_trans … HT0 … HL1) -HT0
-  elim (lpx_fsups_trans … HG2 … HL1) -L
+  elim (lpx_fqus_trans … HG2 … HL1) -L
   /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/
 ] 
 qed-.
@@ -56,5 +56,5 @@ qed.
 theorem fpbsa_inv_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2.
                         ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 *
-/4 width=5 by fpbs_trans, fsups_fpbs, cpxs_fpbs, lpxs_fpbs/
+/4 width=5 by fpbs_trans, fqus_fpbs, cpxs_fpbs, lpxs_fpbs/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
index 7330188e9..2d197c95b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
@@ -89,34 +89,34 @@ lemma lpxs_pair2: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
 
 (* Properties on supclosure *************************************************)
 
-lemma lpxs_fsupq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                        ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
-                        ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
+lemma lpxs_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                       ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
+                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1
 [ /2 width=5 by ex3_2_intro/
 | #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
   lapply (lpx_cpxs_trans … HT1 … HK1) -HT1
-  elim (lpx_fsupq_trans … HT2 … HK1) -K
+  elim (lpx_fquq_trans … HT2 … HK1) -K
   /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/
 ]
 qed-.
 
-lemma lpxs_fsups_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
-                        ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
-                        ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
+lemma lpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                       ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
+                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
 #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
-#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fsupq_trans … H2 … HL0) -L
-#L #T3 #HT3 #HT32 #HL2 elim (fsups_cpxs_trans … HT0 … HT3) -T
-/3 width=7 by cpxs_trans, fsups_strap1, ex3_2_intro/
+#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fquq_trans … H2 … HL0) -L
+#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT0 … HT3) -T
+/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/
 qed-.
 
-lemma lpx_fsups_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
-                       ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
-                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
+lemma lpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                      ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
 #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
-#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fsupq_trans … H2 … HL0) -L
-#L #T3 #HT3 #HT32 #HL2 elim (fsups_cpx_trans … HT0 … HT3) -T
-/3 width=7 by cpxs_strap1, fsups_strap1, ex3_2_intro/
+#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L
+#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T
+/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
index 71c688c21..d1363a3cf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
@@ -36,17 +36,17 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   lapply (ldrop_mono … H … HLK1) -H #H destruct
   elim (cpr_inv_lref1 … H3) -H3
   [1,3: #H destruct
-    lapply (fsupp_lref … G1 … HLK1)
+    lapply (fqup_lref … G1 … HLK1)
     elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
     elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
-    /4 width=10 by da_ldef, da_ldec, fsupp_fpbg/
+    /4 width=10 by da_ldef, da_ldec, fqup_fpbg/
   |2,4: * #K0 #V0 #W0 #H #HVW0 #HW0
     lapply (ldrop_mono … H … HLK1) -H #H destruct
-    lapply (fsupp_lref … G1 … HLK1)
+    lapply (fqup_lref … G1 … HLK1)
     elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
     elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct
     lapply (ldrop_fwd_ldrop2 … HLK2) -V2
-    /4 width=7 by da_lift, fsupp_fpbg/
+    /4 width=7 by da_lift, fqup_fpbg/
   ]
 | #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
   elim (snv_inv_gref … H1)
@@ -55,15 +55,15 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   lapply (da_inv_bind … H2) -H2
   elim (cpr_inv_bind1 … H3) -H3 *
   [ #V2 #T2 #HV12 #HT12 #H destruct
-    /4 width=9 by da_bind, fsupp_fpbg, lpr_pair/
+    /4 width=9 by da_bind, fqup_fpbg, lpr_pair/
   | #T2 #HT12 #HT2 #H1 #H2 destruct
-    /4 width=11 by da_inv_lift, fsupp_fpbg, lpr_pair, ldrop_ldrop/
+    /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_ldrop/
   ]
 | #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct
   elim (snv_inv_appl … H1) -H1 #b0 #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10
   lapply (da_inv_flat … H2) -H2 #Hl
   elim (cpr_inv_appl1 … H3) -H3 *
-  [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fsupp_fpbg/
+  [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fqup_fpbg/
   | #b #V2 #W #W2 #U1 #U2 #HV12 #HW2 #HU12 #H1 #H2 destruct
     elim (snv_inv_bind … HT1) -HT1 #HW #HU1
     lapply (da_inv_bind … Hl) -Hl #Hl
@@ -71,24 +71,24 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     lapply (cprs_div … HW3 … HW10) -W3 #HWW1
     lapply (ssta_da_conf … HVW1 … Hl0) <minus_plus_m_m #H
     elim (snv_fwd_da … HW) #l1 #Hl1
-    lapply (IH3 … HV1 … 1 … Hl0 W1 ?) /2 width=2 by fsupp_fpbg, ssta_lsstas/ #HW1
+    lapply (IH3 … HV1 … 1 … Hl0 W1 ?) /2 width=2 by fqup_fpbg, ssta_lsstas/ #HW1
     lapply (da_cpcs_aux … IH2 IH1 … Hl1 … H … HWW1) -H
-    /3 width=5 by fpbg_fpbs_trans, fsupp_fpbg, ssta_fpbs/ #H destruct
-    lapply (IH1 … HV1 … Hl0 … HV12 … HL12) -HV1 -Hl0 -HV12 [ /2 by fsupp_fpbg/ ] #Hl0
-    lapply (IH1 … Hl1 … HW2 … HL12) -Hl1 // /2 width=1 by fsupp_fpbg/ -HW
-    lapply (IH1 … HU1 … Hl … HU12 (L2.ⓛW2) ?) -IH1 -HU1 -Hl -HU12 [1,2: /2 by fsupp_fpbg, lpr_pair/ ] -HL12 -HW2
+    /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, ssta_fpbs/ #H destruct
+    lapply (IH1 … HV1 … Hl0 … HV12 … HL12) -HV1 -Hl0 -HV12 [ /2 by fqup_fpbg/ ] #Hl0
+    lapply (IH1 … Hl1 … HW2 … HL12) -Hl1 // /2 width=1 by fqup_fpbg/ -HW
+    lapply (IH1 … HU1 … Hl … HU12 (L2.ⓛW2) ?) -IH1 -HU1 -Hl -HU12 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2
     /4 width=6 by da_bind, lsubd_da_trans, lsubd_abbr/
   | #b #V #V2 #W #W2 #U1 #U2 #HV1 #HV2 #HW2 #HU12 #H1 #H2 destruct -IH3 -IH2 -V -W0 -T0 -l0 -HV1 -HVW1
     elim (snv_inv_bind … HT1) -HT1 #_
     lapply (da_inv_bind … Hl) -Hl
-    /5 width=9 by da_bind, da_flat, fsupp_fpbg, lpr_pair/
+    /5 width=9 by da_bind, da_flat, fqup_fpbg, lpr_pair/
   ]
 | #W1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
   elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #Hl0 #HTU1 #HUW1
   lapply (da_inv_flat … H2) -H2 #Hl
   elim (cpr_inv_cast1 … H3) -H3
-  [ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fsupp_fpbg/
-  | /3 width=7 by fsupp_fpbg/
+  [ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fqup_fpbg/
+  | /3 width=7 by fqup_fpbg/
   ]
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
index 4d9c79f3a..bb7ac6ca5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
@@ -82,8 +82,8 @@ qed-.
 
 (* Advanced properties ******************************************************)
 
-lemma snv_fsup_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
-                     ⦃G1, L1⦄ ⊢ T1 ¡[h, g] → ⦃G2, L2⦄ ⊢ T2 ¡[h, g].
+lemma snv_fqu_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                    ⦃G1, L1⦄ ⊢ T1 ¡[h, g] → ⦃G2, L2⦄ ⊢ T2 ¡[h, g].
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
 [ #I1 #G1 #L1 #V1 #H
   elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
index 1b09a0c0a..a9a295a9b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
@@ -34,31 +34,31 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
   elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
   elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
-  lapply (fsupp_lref … G1 … HLK1) #HKL
+  lapply (fqup_lref … G1 … HLK1) #HKL
   elim (cpr_inv_lref1 … H2) -H2
-  [ #H destruct -HLK1 /4 width=10 by fsupp_fpbg, snv_lref/
+  [ #H destruct -HLK1 /4 width=10 by fqup_fpbg, snv_lref/
   | * #K0 #V0 #W0 #H #HVW0 #W0 -HV12
     lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct
-    lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /4 width=7 by fsupp_fpbg, snv_lift/
+    lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, snv_lift/
   ]
 | #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1
   elim (snv_inv_gref … H1)
 | #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2
   elim (snv_inv_bind … H1) -H1 #HV1 #HT1
   elim (cpr_inv_bind1 … H2) -H2 *
-  [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fsupp_fpbg, snv_bind, lpr_pair/
+  [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbg, snv_bind, lpr_pair/
   | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
-    /4 width=10 by fsupp_fpbg, snv_inv_lift, lpr_pair, ldrop_ldrop/
+    /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, ldrop_ldrop/
   ]
 | #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct
   elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU1
   elim (cpr_inv_appl1 … H2) -H2 *
   [ #V2 #T2 #HV12 #HT12 #H destruct -IH4
-    lapply (IH1 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ #HV2
-    lapply (IH1 … HT12 … HL12) /2 width=1 by fsupp_fpbg/ #HT2
-    lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ #H2l0
-    elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fsupp_fpbg/ -HV1 #W2 #HVW2 #HW12
-    elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fsupp_fpbg/ -HT12 -HTU1 #X #HTU2 #H
+    lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+    lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
+    lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #H2l0
+    elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbg/ -HV1 #W2 #HVW2 #HW12
+    elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HT12 -HTU1 #X #HTU2 #H
     elim (cprs_inv_abst1 … H) -H #W20 #U2 #HW120 #_ #H destruct
     lapply (lpr_cprs_conf … HL12 … HW10) -L1 #HW10
     lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120
@@ -70,38 +70,38 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
     elim (cpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
     lapply (cprs_div … HW10 … HW230) -W30 #HW120
-    lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fsupp_fpbg/ #HW10
+    lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbg/ #HW10
     lapply (ssta_da_conf … HVW1 … Hl0) <minus_plus_m_m #HlW10
     elim (snv_fwd_da … HW20) #l #Hl
     lapply (da_cpcs_aux … IH1 IH2 … HlW10 … Hl … HW120) // -HlW10
-    /3 width=5 by fpbg_fpbs_trans, fsupp_fpbg, ssta_fpbs/ #H destruct
-    lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ #HlV2
-    lapply (IH2 … Hl … HW202 … HL12) /2 width=1 by fsupp_fpbg/ #HlW2
-    elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ #W3 #HV2W3 #HW103
+    /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, ssta_fpbs/ #H destruct
+    lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HlV2
+    lapply (IH2 … Hl … HW202 … HL12) /2 width=1 by fqup_fpbg/ #HlW2
+    elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #W3 #HV2W3 #HW103
     lapply (ssta_da_conf … HV2W3 … HlV2) <minus_plus_m_m #HlW3
     lapply (cpcs_cpr_strap1 … HW120 … HW202) -HW120 #HW102
     lapply (lpr_cpcs_conf … HL12 … HW102) -HW102 #HW102
     lapply (cpcs_canc_sn … HW103 … HW102) -W10 #HW32
-    lapply (IH1 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ -HV1 #HV2
-    lapply (IH1 … HW202 … HL12) /2 width=1 by fsupp_fpbg/ -HW20 #HW2
-    lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) /2 width=1 by fsupp_fpbg, lpr_pair/ -HT20 #HT2
+    lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1 #HV2
+    lapply (IH1 … HW202 … HL12) /2 width=1 by fqup_fpbg/ -HW20 #HW2
+    lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT20 #HT2
     lapply (snv_ssta_aux … IH4 … HlV2 … HV2W3)
-    /3 width=5 by fpbg_fpbs_trans, fsupp_fpbg, cpr_lpr_fpbs/ #HW3
+    /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW3
     lapply (lsubsv_snv_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /3 width=3 by snv_bind, snv_cast/
-    @(lsubsv_abbr … l) /3 width=7 by fsupp_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW20
+    @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW20
     lapply (lsstas_ssta_conf_pos … HV2W3 … HV2W) -HV2W #HW3W
     @(lsstas_cpcs_lpr_aux … IH1 IH2 IH3 … HlW3 … HW3W … HlW2 … HW20 … HW32) //
-    [ /3 width=9 by fpbg_fpbs_trans, fsupp_fpbg, cpr_lpr_ssta_fpbs/
-    | /3 width=5 by fpbg_fpbs_trans, fsupp_fpbg, cpr_lpr_fpbs/
+    [ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_ssta_fpbs/
+    | /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/
     ]
   | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -IH4
     elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0
     elim (cpds_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
     elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
     lapply (lpr_cprs_conf … HL12 … HW10) -HW10 #HW10
-    elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fsupp_fpbg, lpr_pair/ -HTU0 #X #HTU2 #H
+    elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HTU2 #H
     elim (cprs_inv_abst1 … H) -H #W #U2 #HW1 #_ #H destruct -U3
-    elim (ssta_cpr_lpr_aux … IH3 … HVW1 … HV10 … HL12) /2 width=2 by fsupp_fpbg/ -IH3 -HVW1 #X #H1 #H2
+    elim (ssta_cpr_lpr_aux … IH3 … HVW1 … HV10 … HL12) /2 width=2 by fqup_fpbg/ -IH3 -HVW1 #X #H1 #H2
     lapply (cpcs_canc_sn … H2 HW10) -W10 #H2
     elim (lift_total X 0 1) #W20 #H3
     lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=1 by ldrop_ldrop/ -H1 #HVW20
@@ -109,11 +109,11 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20
     elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3
     lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) /2 width=1 by cprs_bind/ -HW3 -HTU2 #HTU2
-    lapply (IH2 … Hl0 … HV10 … HL12) /2 width=1 by fsupp_fpbg/ -IH2 -Hl0 #Hl0
+    lapply (IH2 … Hl0 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -Hl0 #Hl0
     lapply (da_lift … Hl0 (L2.ⓓW2) … HV02) /2 width=1 by ldrop_ldrop/ -Hl0 #Hl0
-    lapply (IH1 … HW02 … HL12) /2 width=1 by fsupp_fpbg/ -HW0 #HW2
-    lapply (IH1 … HV10 … HL12) /2 width=1 by fsupp_fpbg/ -HV1 -HV10 #HV0
-    lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fsupp_fpbg, lpr_pair/ -L1 #HT2
+    lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ -HW0 #HW2
+    lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV10 #HV0
+    lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -L1 #HT2
     lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /3 width=7 by snv_bind, snv_appl, ldrop_ldrop/
   ]
 | #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4
@@ -121,13 +121,13 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   elim (cpr_inv_cast1 … H2) -H2
   [ * #W2 #T2 #HW12 #HT12 #H destruct
     lapply (cpcs_cprs_strap1 … HUW1 W2 ?) /2 width=1 by cpr_cprs/ -HUW1 #H1
-    lapply (IH1 … HW12 … HL12) /2 width=1 by fsupp_fpbg/ -HW1 -HW12 #HW2
-    lapply (IH1 … HT12 … HL12) /2 width=1 by fsupp_fpbg/ -IH1 #HT2
-    elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HTU1 … HT12 … HL12) /2 width=2 by fsupp_fpbg/ -IH3 -HTU1 #U2 #HTU2 #HU12
-    lapply (IH2 … Hl0 … HT12 … HL12) /2 width=1 by fsupp_fpbg/ -IH2 -HT1 -HT12 -Hl0 #Hl0
+    lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ -HW1 -HW12 #HW2
+    lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -IH1 #HT2
+    elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HTU1 … HT12 … HL12) /2 width=2 by fqup_fpbg/ -IH3 -HTU1 #U2 #HTU2 #HU12
+    lapply (IH2 … Hl0 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -HT1 -HT12 -Hl0 #Hl0
     /4 width=7 by snv_cast, lpr_cpcs_conf, cpcs_canc_sn/
   | #H -IH3 -IH2 -HW1 -HTU1 -HUW1
-    lapply (IH1 … H … HL12) /2 width=1 by fsupp_fpbg/
+    lapply (IH1 … H … HL12) /2 width=1 by fqup_fpbg/
   ]
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma
index 1656a6422..ac5dc04cd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma
@@ -36,20 +36,20 @@ fact snv_lsstas_aux: ∀h,g,G0,L0,T0.
   elim (lsstas_inv_lref1 … H2) -H2 * #K0 #Y0 #X0 [2,4: #l0 ] #HLK0 [1,2: #HYl0 ] #HYX0 #HX0
   lapply (ldrop_mono … HLK0 … HLK1) -HLK0 #H destruct
   [ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 ]
-  lapply (fsupp_lref … G1 … HLK1) #H
-  lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=8 by fsupp_fpbg, snv_lift/
+  lapply (fqup_lref … G1 … HLK1) #H
+  lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/
 | #p #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
   elim (snv_inv_gref … H1)
 | #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2
   elim (snv_inv_bind … H1) -H1 #HV1 #HT1
   lapply (da_inv_bind … Hl1) -Hl1 #Hl1
-  elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fsupp_fpbg, snv_bind/
+  elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbg, snv_bind/
 | #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct
   elim (snv_inv_appl … H1) -H1 #a #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10
   lapply (da_inv_flat … Hl1) -Hl1 #Hl1
   elim (lsstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct
-  lapply (IH1 … HT1 … Hl1 … HTU1) /2 width=1 by fsupp_fpbg/ #HU1
-  elim (lsstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HTU1 … HT10) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fsupp_fpbg/ -T1 -l1 #X #l #_ #H #HU10 -l2
+  lapply (IH1 … HT1 … Hl1 … HTU1) /2 width=1 by fqup_fpbg/ #HU1
+  elim (lsstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HTU1 … HT10) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -l1 #X #l #_ #H #HU10 -l2
   elim (lsstas_inv_bind1 … H) -H #U0 #_ #H destruct -T0 -l
   elim (cpes_inv_abst2 … HU10) -HU10 #W2 #U2 #HU12 #HU02
   elim (cprs_inv_abst … HU02) -HU02 #HW02 #_
@@ -58,6 +58,6 @@ fact snv_lsstas_aux: ∀h,g,G0,L0,T0.
   [ lapply (lsstas_inv_O … H2) -H2 #H destruct // ]
   elim (snv_inv_cast … H1) -H1
   lapply (da_inv_flat … Hl1) -Hl1
-  lapply (lsstas_inv_cast1 … H2) -H2 /3 width=8 by fsupp_fpbg/
+  lapply (lsstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbg/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
index 6b64401fb..5166e92a2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
@@ -42,7 +42,7 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   [ lapply (da_mono … Hl … HWl1) -Hl #H destruct
     lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21
   ]
-  lapply (fsupp_lref … G1 … HLK1) #HKV1
+  lapply (fqup_lref … G1 … HLK1) #HKV1
   elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
   elim (lpr_inv_pair1 … H) -H #K2 [ #W2 | #V2 ] #HK12 [ #HW12 | #HV12 ] #H destruct
   lapply (ldrop_fwd_ldrop2 … HLK2) #H2
@@ -51,13 +51,13 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   |2,4: * #K0 #V0 #X0 #H #HVX0 #HX0
         lapply (ldrop_mono … H … HLK1) -H -HLK1 #H destruct
   ]
-  [ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fsupp_fpbg/ #V2 #HWV2 #HV2
+  [ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2
     elim (lift_total V2 0 (i+1))
-    /6 width=11 by fsupp_fpbg, cpcs_lift, lsstas_ldec, ex2_intro/
-  | elim (IH1 … HVl1 … HW0 … HV12 … HK12) -IH1 -HVl1 -HW0 -HV12 -HK12 -IH2 /2 width=1 by fsupp_fpbg/ #W2 #HVW2 #HW02
+    /6 width=11 by fqup_fpbg, cpcs_lift, lsstas_ldec, ex2_intro/
+  | elim (IH1 … HVl1 … HW0 … HV12 … HK12) -IH1 -HVl1 -HW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbg/ #W2 #HVW2 #HW02
     elim (lift_total W2 0 (i+1))
     /4 width=11 by cpcs_lift, lsstas_ldef, ex2_intro/
-  | elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fsupp_fpbg/ -l1 #W2 #HXW2 #HW02
+  | elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -l1 #W2 #HXW2 #HW02
     elim (lift_total W2 0 (i+1))
     /3 width=11 by cpcs_lift, lsstas_lift, ex2_intro/
   ]
@@ -69,10 +69,10 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct
   elim (cpr_inv_bind1 … H3) -H3 *
   [ #V2 #T2 #HV12 #HT12 #H destruct
-    elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fsupp_fpbg, lpr_pair/ -T1
+    elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fqup_fpbg, lpr_pair/ -T1
     /4 width=5 by cpcs_bind2, lpr_cpr_conf, lsstas_bind, ex2_intro/
   | #T3 #HT13 #HXT3 #H1 #H2 destruct
-    elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fsupp_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13
+    elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13
     elim (lsstas_inv_lift1 … HTU3 L2 … HXT3) -T3
     /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_ldrop, ex2_intro/
   ]
@@ -83,7 +83,7 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   elim (cpr_inv_appl1 … H3) -H3 *
   [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH4 -IH3 -IH2
     elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1
-    /4 width=5 by fsupp_fpbg, cpcs_flat, lpr_cpr_conf, lsstas_appl, ex2_intro/
+    /4 width=5 by fqup_fpbg, cpcs_flat, lpr_cpr_conf, lsstas_appl, ex2_intro/
   | #b #V2 #W2 #W3 #T2 #T3 #HV12 #HW23 #HT23 #H1 #H2 destruct
     elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2
     lapply (da_inv_bind … Hl1) -Hl1 #Hl1
@@ -92,18 +92,18 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     lapply (cprs_div … HW10 … HW20) -W0 #HW12
     lapply (ssta_da_conf … HVW1 … Hl0) <minus_plus_m_m #H
     elim (snv_fwd_da … HW2) #l #Hl
-    lapply (IH4 … HV1 … 1 … Hl0 W1 ?) /2 width=1 by fsupp_fpbg, ssta_lsstas/ #HW1
+    lapply (IH4 … HV1 … 1 … Hl0 W1 ?) /2 width=1 by fqup_fpbg, ssta_lsstas/ #HW1
     lapply (da_cpcs_aux … IH3 IH2 … H … Hl … HW12) // -H
-    /3 width=5 by fpbg_fpbs_trans, fsupp_fpbg, ssta_fpbs/ #H destruct
-    lapply (IH3 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ #HV2
-    lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ #HV2l
-    elim (IH1 … 1 … Hl0 … W1 … HV12 … HL12) /2 width=1 by fsupp_fpbg, ssta_lsstas/ -HVW1 #W4 #H #HW14
+    /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, ssta_fpbs/ #H destruct
+    lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+    lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2l
+    elim (IH1 … 1 … Hl0 … W1 … HV12 … HL12) /2 width=1 by fqup_fpbg, ssta_lsstas/ -HVW1 #W4 #H #HW14
     lapply (lsstas_inv_SO … H) #HV2W4
     lapply (ssta_da_conf … HV2W4 … HV2l) <minus_plus_m_m #HW4l
-    lapply (IH4 … HV2 … HV2l … H) -H /3 width=5 by fpbg_fpbs_trans, fsupp_fpbg, cpr_lpr_fpbs/ #HW4
-    lapply (IH3 … HW23 … HL12) /2 width=1 by fsupp_fpbg/ #HW3
-    lapply (IH2 … Hl … HW23 … HL12) /2 width=1 by fsupp_fpbg/ #HW3l
-    elim (IH1 … Hl1 … HTU2 … HT23 (L2.ⓛW3)) -HTU2 /2 width=1 by fsupp_fpbg, lpr_pair/ #U3 #HTU3 #HU23
+    lapply (IH4 … HV2 … HV2l … H) -H /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW4
+    lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3
+    lapply (IH2 … Hl … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3l
+    elim (IH1 … Hl1 … HTU2 … HT23 (L2.ⓛW3)) -HTU2 /2 width=1 by fqup_fpbg, lpr_pair/ #U3 #HTU3 #HU23
     lapply (cpcs_cpr_strap1 … HW12 … HW23) #H
     lapply (lpr_cpcs_conf … HL12 … H) -H #H
     lapply (cpcs_canc_sn … HW14 H) -H #HW43
@@ -114,20 +114,20 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
       @(cpcs_cpr_strap1 … (ⓐV2.ⓛ{b}W3.U3)) /2 width=1 by cpr_beta/
       /4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/
     | -U3
-      @(lsubsv_abbr … l) /3 width=7 by fsupp_fpbg/
+      @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/
       #W #W0 #l0 #Hl0 #HV2W #HW30
       lapply (lsstas_ssta_conf_pos … HV2W4 … HV2W) -HV2W #HW4W
       @(lsstas_cpcs_lpr_aux … IH3 IH2 IH1 … Hl0 … HW4W … Hl0 … HW30 … HW43) //
-      [ /3 width=9 by fpbg_fpbs_trans, fsupp_fpbg, cpr_lpr_ssta_fpbs/
-      | /3 width=5 by fpbg_fpbs_trans, fsupp_fpbg, cpr_lpr_fpbs/
+      [ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_ssta_fpbs/
+      | /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/
       ]
-    | -IH1 -IH3 -IH4 /3 width=9 by fsupp_fpbg, lpr_pair/
+    | -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbg, lpr_pair/
     ]
   | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -a -l0 -W1 -W10 -HV1 -IH4 -IH3 -IH2
     elim (snv_inv_bind … HT1) -HT1 #_ #HT0
     lapply (da_inv_bind … Hl1) -Hl1 #Hl1
     elim (lsstas_inv_bind1 … HTU1) -HTU1 #U0 #HTU0 #H destruct
-    elim (IH1 … Hl1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -Hl1 -HTU0 /2 width=1 by fsupp_fpbg, lpr_pair/ -T0 #U2 #HTU2 #HU02
+    elim (IH1 … Hl1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -Hl1 -HTU0 /2 width=1 by fqup_fpbg, lpr_pair/ -T0 #U2 #HTU2 #HU02
     lapply (lpr_cpr_conf … HL12 … HV10) -HV10 #HV10
     lapply (lpr_cpr_conf … HL12 … HW02) -L1 #HW02
     lapply (cpcs_bind2 b … HW02 … HU02) -HW02 -HU02 #HU02
@@ -143,10 +143,10 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   elim (cpr_inv_cast1 … H3) -H3
   [ * #U2 #T2 #_ #HT12 #H destruct
     elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1 -HL12
-    /3 width=3 by fsupp_fpbg, lsstas_cast, ex2_intro/
+    /3 width=3 by fqup_fpbg, lsstas_cast, ex2_intro/
   | #HT1X3
     elim (IH1 … Hl1 … HTU1 … HT1X3 … HL12) -IH1 -Hl1 -HTU1 -HL12
-    /2 width=3 by fsupp_fpbg, ex2_intro/
+    /2 width=3 by fqup_fpbg, ex2_intro/
   ]
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
index deb838412..e8ecc622c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
@@ -85,7 +85,7 @@ lemma cpcs_cpr_conf: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄
 (* Basic_1: removed theorems 9:
             clear_pc3_trans pc3_ind_left
             pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21
-            pc3_pr2_fsubst0 pc3_pr2_fsubst0_back pc3_fsubst0
+            pc3_pr2_fqubst0 pc3_pr2_fqubst0_back pc3_fqubst0
             pc3_gen_abst pc3_gen_abst_shift
 *)
 (* Basic_1: removed local theorems 6:
diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt
index 57b97d1d5..5530ee711 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/names.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt
@@ -76,6 +76,7 @@ e: decomposed extended conversion
 q: restricted reduction
 r: reduction
 s: substitution
+u: supclosure
 x: extended reduction
 
 - forth letter (if present)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
index aabc8d9b4..6dd309deb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/relocation/ldrop_ldrop.ma".
-include "basic_2/relocation/fsupq_alt.ma".
+include "basic_2/relocation/fquq_alt.ma".
 include "basic_2/static/ssta.ma".
 include "basic_2/reduction/cpx.ma".
 
@@ -138,37 +138,37 @@ qed-.
 
 (* Properties on supclosure *************************************************)
 
-lemma fsup_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
-                      ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
-                      ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
+lemma fqu_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                     ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
+                     ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 
-/3 width=3 by fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, cpx_pair_sn, cpx_bind, cpx_flat, ex2_intro/
+/3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, cpx_pair_sn, cpx_bind, cpx_flat, ex2_intro/
 [ #I #G #L #V2 #U2 #HVU2
   elim (lift_total U2 0 1)
-  /4 width=9 by fsup_drop, cpx_append, cpx_delta, ldrop_pair, ldrop_ldrop, ex2_intro/
+  /4 width=9 by fqu_drop, cpx_append, cpx_delta, ldrop_pair, ldrop_ldrop, ex2_intro/
 | #G #L #K #T1 #U1 #e #HLK1 #HTU1 #T2 #HTU2
   elim (lift_total T2 0 (e+1))
-  /3 width=11 by cpx_lift, fsup_drop, ex2_intro/
+  /3 width=11 by cpx_lift, fqu_drop, ex2_intro/
 ]
 qed-.
 
-lemma fsup_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
-                       ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h, g] U2 →
-                       ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
-                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
-/3 width=5 by fsup_cpx_trans, ssta_cpx/ qed-.
+lemma fqu_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                      ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h, g] U2 →
+                      ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
+                      ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
+/3 width=5 by fqu_cpx_trans, ssta_cpx/ qed-.
 
-lemma fsupq_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                       ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
-                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fsupq_inv_gen … H) -H
-[ #HT12 elim (fsup_cpx_trans … HT12 … HTU2) /3 width=3 by fsup_fsupq, ex2_intro/
+lemma fquq_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                      ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
+                      ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_cpx_trans … HT12 … HTU2) /3 width=3 by fqu_fquq, ex2_intro/
 | * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
 ]
 qed-.
 
-lemma fsupq_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                        ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h, g] U2 →
-                        ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
-                        ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
-/3 width=5 by fsupq_cpx_trans, ssta_cpx/ qed-.
+lemma fquq_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                       ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h, g] U2 →
+                       ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
+                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
+/3 width=5 by fquq_cpx_trans, ssta_cpx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma
index 734e7b597..05bd28248 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma
@@ -13,15 +13,15 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/btpred_8.ma".
-include "basic_2/relocation/fsupq.ma".
+include "basic_2/relocation/fquq.ma".
 include "basic_2/reduction/lpx.ma".
 
 (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************)
 
 inductive fpb (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpb_fsupq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2
-| fpb_cpx  : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → fpb h g G1 L1 T1 G1 L1 T2
-| fpb_lpx  : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → fpb h g G1 L1 T1 G1 L2 T1
+| fpb_fquq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2
+| fpb_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → fpb h g G1 L1 T1 G1 L1 T2
+| fpb_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → fpb h g G1 L1 T1 G1 L2 T1
 .
 
 interpretation
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma
index a2b62d2a1..cb391a6c9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma
@@ -13,14 +13,14 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/btpredproper_8.ma".
-include "basic_2/relocation/fsupq_alt.ma".
+include "basic_2/relocation/fquq_alt.ma".
 include "basic_2/reduction/fpb.ma".
 
 (* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************)
 
 inductive fpbc (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpbc_fsup  : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → fpbc h g G1 L1 T1 G2 L2 T2
-| fpbc_cpx   : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → fpbc h g G1 L1 T1 G1 L1 T2
+| fpbc_fqu: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → fpbc h g G1 L1 T1 G2 L2 T2
+| fpbc_cpx: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → fpbc h g G1 L1 T1 G1 L1 T2
 .
 
 interpretation
@@ -30,24 +30,24 @@ interpretation
 (* Basic properties *********************************************************)
 
 lemma fpbc_fpb: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
-               ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄.
+                ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-/3 width=1 by fpb_fsupq, fpb_cpx, fsup_fsupq/
+/3 width=1 by fpb_fquq, fpb_cpx, fqu_fquq/
 qed.
 
 lemma cpr_fpbc: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) →
-               ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
+                ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
 /3 width=1 by fpbc_cpx, cpr_cpx/ qed.
 
 (* Inversion lemmas on "big tree" parallel reduction for closures ***********)
 
 lemma fpb_inv_fpbc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
-                   ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨
-                   ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡[h, g] L2 & T1 = T2.
+                    ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨
+                    ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡[h, g] L2 & T1 = T2.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
 /3 width=1 by and3_intro, or_intror/
-[ #G2 #L2 #T2 #H elim (fsupq_inv_gen … H) -H [| * ]
-  /3 width=1 by fpbc_fsup, and3_intro, or_introl, or_intror/
+[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H [| * ]
+  /3 width=1 by fpbc_fqu, and3_intro, or_introl, or_intror/
 | #T2 #HT12 elim (term_eq_dec T1 T2) #H destruct
   /4 width=1 by and3_intro, or_introl, or_intror, fpbc_cpx/
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma
index cfc7cd7f3..29bc6a975 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/relocation/fsupq_alt.ma".
+include "basic_2/relocation/fquq_alt.ma".
 include "basic_2/relocation/ldrop_lpx_sn.ma".
 include "basic_2/reduction/cpr_lift.ma".
 include "basic_2/reduction/lpr.ma".
@@ -34,21 +34,21 @@ lemma lpr_ldrop_trans_O1: ∀G. dropable_dx (lpr G).
 
 (* Properties on context-sensitive parallel reduction for terms *************)
 
-lemma fsup_cpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
-                      ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
-                      ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃ ⦃G2, L2, U2⦄.
+lemma fqu_cpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                     ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
+                     ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃ ⦃G2, L2, U2⦄.
 #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=5 by fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/
+/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/
 #G #L #K #U #T #e #HLK #HUT #U2 #HU2
 elim (lift_total U2 0 (e+1)) #T2 #HUT2
-lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fsup_drop, ex3_2_intro/
+lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fqu_drop, ex3_2_intro/
 qed-.
 
-lemma fsupq_cpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                       ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
-                       ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fsupq_inv_gen … H) -H
-[ #HT12 elim (fsup_cpr_trans … HT12 … HTU2) /3 width=5 by fsup_fsupq, ex3_2_intro/
+lemma fquq_cpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                      ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
+                      ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_cpr_trans … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/
 | * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
 ]
 qed-.
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 5d4c47072..addc2f948 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/grammar/lpx_sn_lpx_sn.ma".
-include "basic_2/substitution/fsupp.ma".
+include "basic_2/substitution/fqup.ma".
 include "basic_2/reduction/lpr_ldrop.ma".
 
 (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
@@ -41,7 +41,7 @@ elim (lpr_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
 elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
 elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
 lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
-lapply (fsupp_lref … G … HLK0) -HLK0 #HLK0
+lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
 elim (lift_total V 0 (i+1)) #T #HVT
 lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
@@ -70,7 +70,7 @@ lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1
 elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
 elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
 lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
-lapply (fsupp_lref … G … HLK0) -HLK0 #HLK0
+lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
 elim (lift_total V 0 (i+1)) #T #HVT
 lapply (cpr_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
@@ -278,7 +278,7 @@ lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1/
 qed-.
 
 theorem cpr_conf_lpr: ∀G. lpx_sn_confluent (cpr G) (cpr G).
-#G #L0 #T0 @(fsupp_wf_ind … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [|*]
+#G #L0 #T0 @(fqup_wf_ind … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [|*]
 [ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
   elim (cpr_inv_atom1 … H1) -H1
   elim (cpr_inv_atom1 … H2) -H2
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
index 9848968d7..705d5695e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
@@ -31,48 +31,48 @@ lemma lpx_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpx h g G).
 
 (* Properties on supclosure *************************************************)
 
-lemma fsup_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
-                      ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
-                      ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄.
+lemma fqu_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                     ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
+                     ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=5 by fsup_lref_O, fsup_pair_sn, fsup_flat_dx, lpx_pair, ex3_2_intro/
+/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpx_pair, ex3_2_intro/
 [ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H
   #K2 #W2 #HLK2 #HVW2 #H destruct
-  /3 width=5 by fsup_fsupq, cpx_pair_sn, fsup_bind_dx, ex3_2_intro/
+  /3 width=5 by fqu_fquq, cpx_pair_sn, fqu_bind_dx, ex3_2_intro/
 | #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12
   elim (ldrop_lpx_trans … HLK1 … HK12) -HK12
-  /3 width=7 by fsup_drop, ex3_2_intro/
+  /3 width=7 by fqu_drop, ex3_2_intro/
 ]
 qed-.
 
-lemma fsupq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                       ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
-                       ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fsupq_inv_gen … H) -H
-[ #HT12 elim (fsup_lpx_trans … HT12 … HLK2) /3 width=5 by fsup_fsupq, ex3_2_intro/
+lemma fquq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                      ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
+                      ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_lpx_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
 | * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
 ]
 qed-.
 
-lemma lpx_fsup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
-                      ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
-                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+lemma lpx_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                     ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+                     ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=7 by fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, lpx_pair, ex3_2_intro/
+/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/
 [ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H
   #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
-  /4 width=7 by cpx_delta, fsup_drop, ldrop_ldrop, ex3_2_intro/
+  /4 width=7 by cpx_delta, fqu_drop, ldrop_ldrop, ex3_2_intro/
 | #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01
   elim (lpx_ldrop_trans_O1 … HL01 … HLK1) -L1
-  /3 width=5 by fsup_drop, ex3_2_intro/
+  /3 width=5 by fqu_drop, ex3_2_intro/
 ]
 qed-.
 
-lemma lpx_fsupq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                       ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
-                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fsupq_inv_gen … H) -H
-[ #HT12 elim (lpx_fsup_trans … HT12 … HKL1) /3 width=5 by fsup_fsupq, ex3_2_intro/
+lemma lpx_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                      ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (lpx_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/
 | * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma
similarity index 60%
rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma
index 9719b4992..41c68deaf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma
@@ -19,33 +19,33 @@ include "basic_2/relocation/ldrop.ma".
 (* SUPCLOSURE ***************************************************************)
 
 (* activate genv *)
-inductive fsup: tri_relation genv lenv term ≝
-| fsup_lref_O : ∀I,G,L,V. fsup G (L.ⓑ{I}V) (#0) G L V
-| fsup_pair_sn: ∀I,G,L,V,T. fsup G L (②{I}V.T) G L V
-| fsup_bind_dx: ∀a,I,G,L,V,T. fsup G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
-| fsup_flat_dx: ∀I,G,L,V,T. fsup G L (ⓕ{I}V.T) G L T
-| fsup_drop   : ∀G,L,K,T,U,e.
-                ⇩[0, e+1] L ≡ K → ⇧[0, e+1] T ≡ U → fsup G L U G K T
+inductive fqu: tri_relation genv lenv term ≝
+| fqu_lref_O : ∀I,G,L,V. fqu G (L.ⓑ{I}V) (#0) G L V
+| fqu_pair_sn: ∀I,G,L,V,T. fqu G L (②{I}V.T) G L V
+| fqu_bind_dx: ∀a,I,G,L,V,T. fqu G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
+| fqu_flat_dx: ∀I,G,L,V,T. fqu G L (ⓕ{I}V.T) G L T
+| fqu_drop   : ∀G,L,K,T,U,e.
+               ⇩[0, e+1] L ≡ K → ⇧[0, e+1] T ≡ U → fqu G L U G K T
 .
 
 interpretation
    "structural successor (closure)"
-   'SupTerm G1 L1 T1 G2 L2 T2 = (fsup G1 L1 T1 G2 L2 T2).
+   'SupTerm G1 L1 T1 G2 L2 T2 = (fqu G1 L1 T1 G2 L2 T2).
 
 (* Basic properties *********************************************************)
 
-lemma fsup_drop_lt: ∀G,L,K,T,U,e. 0 < e →
-                    ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fsup G L U G K T.
-#G #L #K #T #U #e #He >(plus_minus_m_m e 1) /2 width=3 by fsup_drop/
+lemma fqu_drop_lt: ∀G,L,K,T,U,e. 0 < e →
+                   ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fqu G L U G K T.
+#G #L #K #T #U #e #He >(plus_minus_m_m e 1) /2 width=3 by fqu_drop/
 qed.
 
-lemma fsup_lref_S_lt: ∀I,G,L,V,i. 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊃ ⦃G, L, #(i-1)⦄.
-/3 width=3 by fsup_drop, ldrop_ldrop, lift_lref_ge_minus/
+lemma fqu_lref_S_lt: ∀I,G,L,V,i. 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊃ ⦃G, L, #(i-1)⦄.
+/3 width=3 by fqu_drop, ldrop_ldrop, lift_lref_ge_minus/
 qed.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma fsup_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}.
+lemma fqu_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}.
 #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 //
 #G #L #K #T #U #e #HLK #HTU
 lapply (ldrop_fwd_lw_lt … HLK ?) -HLK // #HKL
@@ -53,8 +53,8 @@ lapply (lift_fwd_tw … HTU) -e #H
 normalize in ⊢ (?%%); /2 width=1 by lt_minus_to_plus/
 qed-.
 
-fact fsup_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
-                                ∀i. T1 = #i → |L2| < |L1|.
+fact fqu_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                               ∀i. T1 = #i → |L2| < |L1|.
 #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
 [1: normalize //
 |3: #a
@@ -62,6 +62,6 @@ fact fsup_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2
 ] #I #G #L #V #T #j #H destruct
 qed-.
 
-lemma fsup_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃ ⦃G2, L2, T2⦄ → |L2| < |L1|.
-/2 width=7 by fsup_fwd_length_lref1_aux/
+lemma fqu_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃ ⦃G2, L2, T2⦄ → |L2| < |L1|.
+/2 width=7 by fqu_fwd_length_lref1_aux/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma
similarity index 61%
rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma
index 0a48ca02a..de000da70 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma
@@ -13,36 +13,36 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/suptermopt_6.ma".
-include "basic_2/relocation/fsup.ma".
+include "basic_2/relocation/fqu.ma".
 
 (* OPTIONAL SUPCLOSURE ******************************************************)
 
 (* activate genv *)
-inductive fsupq: tri_relation genv lenv term ≝
-| fsupq_lref_O : ∀I,G,L,V. fsupq G (L.ⓑ{I}V) (#0) G L V
-| fsupq_pair_sn: ∀I,G,L,V,T. fsupq G L (②{I}V.T) G L V
-| fsupq_bind_dx: ∀a,I,G,L,V,T. fsupq G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
-| fsupq_flat_dx: ∀I,G, L,V,T. fsupq G L (ⓕ{I}V.T) G L T
-| fsupq_drop   : ∀G,L,K,T,U,e.
-                 ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fsupq G L U G K T
+inductive fquq: tri_relation genv lenv term ≝
+| fquq_lref_O : ∀I,G,L,V. fquq G (L.ⓑ{I}V) (#0) G L V
+| fquq_pair_sn: ∀I,G,L,V,T. fquq G L (②{I}V.T) G L V
+| fquq_bind_dx: ∀a,I,G,L,V,T. fquq G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
+| fquq_flat_dx: ∀I,G, L,V,T. fquq G L (ⓕ{I}V.T) G L T
+| fquq_drop   : ∀G,L,K,T,U,e.
+                ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fquq G L U G K T
 .
 
 interpretation
    "optional structural successor (closure)"
-   'SupTermOpt G1 L1 T1 G2 L2 T2 = (fsupq G1 L1 T1 G2 L2 T2).
+   'SupTermOpt G1 L1 T1 G2 L2 T2 = (fquq G1 L1 T1 G2 L2 T2).
 
 (* Basic properties *********************************************************)
 
-lemma fsupq_refl: tri_reflexive … fsupq.
-/2 width=3 by fsupq_drop/ qed.
+lemma fquq_refl: tri_reflexive … fquq.
+/2 width=3 by fquq_drop/ qed.
 
-lemma fsup_fsupq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // /2 width=3 by fsupq_drop/
+lemma fqu_fquq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // /2 width=3 by fquq_drop/
 qed.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma fsupq_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}.
+lemma fquq_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}.
 #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 /2 width=1 by lt_to_le/
 #G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1
 lapply (ldrop_fwd_lw … HLK1) -HLK1
@@ -50,8 +50,8 @@ lapply (lift_fwd_tw … HTU1) -HTU1
 /2 width=1 by le_plus, le_n/
 qed-.
 
-fact fsupq_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                                 ∀i. T1 = #i → |L2| ≤ |L1|.
+fact fquq_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                                ∀i. T1 = #i → |L2| ≤ |L1|.
 #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 //
 [ #a #I #G #L #V #T #j #H destruct
 | #G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #i #H destruct
@@ -59,6 +59,6 @@ fact fsupq_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ 
 ]
 qed-.
 
-lemma fsupq_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃⸮ ⦃G2, L2, T2⦄ → |L2| ≤ |L1|.
-/2 width=7 by fsupq_fwd_length_lref1_aux/
+lemma fquq_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃⸮ ⦃G2, L2, T2⦄ → |L2| ≤ |L1|.
+/2 width=7 by fquq_fwd_length_lref1_aux/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma
similarity index 61%
rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma
index cfbca8693..1d770dcc4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma
@@ -13,47 +13,47 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/suptermoptalt_6.ma".
-include "basic_2/relocation/fsupq.ma".
+include "basic_2/relocation/fquq.ma".
 
 (* OPTIONAL SUPCLOSURE ******************************************************)
 
-(* alternative definition of fsupq *)
-definition fsupqa: tri_relation genv lenv term ≝ tri_RC … fsup.
+(* alternative definition of fquq *)
+definition fquqa: tri_relation genv lenv term ≝ tri_RC … fqu.
 
 interpretation
    "optional structural successor (closure) alternative"
-   'SupTermOptAlt G1 L1 T1 G2 L2 T2 = (fsupqa G1 L1 T1 G2 L2 T2).
+   'SupTermOptAlt G1 L1 T1 G2 L2 T2 = (fquqa G1 L1 T1 G2 L2 T2).
 
 (* Basic properties *********************************************************)
 
-lemma fsupqa_refl: tri_reflexive … fsupqa.
+lemma fquqa_refl: tri_reflexive … fquqa.
 // qed.
 
-lemma fsupqa_drop: ∀G,L,K,T,U,e.
-                   ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄.
+lemma fquqa_drop: ∀G,L,K,T,U,e.
+                  ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄.
 #G #L #K #T #U #e #HLK #HTU elim (eq_or_gt e)
-/3 width=5 by fsup_drop_lt, or_introl/ #H destruct
+/3 width=5 by fqu_drop_lt, or_introl/ #H destruct
 >(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T //
 qed.
 
 (* Main properties **********************************************************)
 
-theorem fsupq_fsupqa: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄.
+theorem fquq_fquqa: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄.
 #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/2 width=3 by fsupqa_drop, fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, or_introl/
+/2 width=3 by fquqa_drop, fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, or_introl/
 qed.
 
 (* Main inversion properties ************************************************)
 
-theorem fsupqa_inv_fsupq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H /2 width=1 by fsup_fsupq/
+theorem fquqa_inv_fquq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H /2 width=1 by fqu_fquq/
 * #H1 #H2 #H3 destruct //
 qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma fsupq_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ ∨ (∧∧ G1 = G2 & L1 = L2 & T1 = T2).
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fsupq_fsupqa … H) -H [| * ]
+lemma fquq_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                    ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ ∨ (∧∧ G1 = G2 & L1 = L2 & T1 = T2).
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fquq_fquqa … H) -H [| * ]
 /2 width=1 by or_introl/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma
new file mode 100644
index 000000000..c4c26fde2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma
@@ -0,0 +1,102 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/relations/suptermplus_6.ma".
+include "basic_2/relocation/fqu.ma".
+
+(* PLUS-ITERATED SUPCLOSURE *************************************************)
+
+definition fqup: tri_relation genv lenv term ≝ tri_TC … fqu.
+
+interpretation "plus-iterated structural successor (closure)"
+   'SupTermPlus G1 L1 T1 G2 L2 T2 = (fqup G1 L1 T1 G2 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fqu_fqup: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
+/2 width=1 by tri_inj/ qed.
+
+lemma fqup_strap1: ∀G1,G,G2,L1,L,L2,T1,T,T2.
+                   ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃ ⦃G2, L2, T2⦄ →
+                   ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
+/2 width=5 by tri_step/ qed.
+
+lemma fqup_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2.
+                   ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃+ ⦃G2, L2, T2⦄ →
+                   ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
+/2 width=5 by tri_TC_strap/ qed.
+
+lemma fqup_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
+                  ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ → ⦃G1, L1, U1⦄ ⊃+ ⦃G2, K2, T2⦄.
+#G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #e #HLK1 #HTU1 #HT12 elim (eq_or_gt … e) #H destruct
+[ >(ldrop_inv_O2 … HLK1) -L1 <(lift_inv_O2 … HTU1) -U1 //
+| /3 width=5 by fqup_strap2, fqu_drop_lt/
+]
+qed-.
+
+lemma fqup_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃+ ⦃G, K, V⦄.
+/3 width=6 by fqu_lref_O, fqu_fqup, lift_lref_ge, fqup_ldrop/ qed.
+
+lemma fqup_pair_sn: ∀I,G,L,V,T. ⦃G, L, ②{I}V.T⦄ ⊃+ ⦃G, L, V⦄.
+/2 width=1 by fqu_pair_sn, fqu_fqup/ qed.
+
+lemma fqup_bind_dx: ∀a,I,G,L,V,T. ⦃G, L, ⓑ{a,I}V.T⦄ ⊃+ ⦃G, L.ⓑ{I}V, T⦄.
+/2 width=1 by fqu_bind_dx, fqu_fqup/ qed.
+
+lemma fqup_flat_dx: ∀I,G,L,V,T. ⦃G, L, ⓕ{I}V.T⦄ ⊃+ ⦃G, L, T⦄.
+/2 width=1 by fqu_flat_dx, fqu_fqup/ qed.
+
+lemma fqup_flat_dx_pair_sn: ∀I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.②{I2}V2.T⦄ ⊃+ ⦃G, L, V2⦄.
+/2 width=5 by fqu_pair_sn, fqup_strap1/ qed.
+
+lemma fqup_bind_dx_flat_dx: ∀a,G,I1,I2,L,V1,V2,T. ⦃G, L, ⓑ{a,I1}V1.ⓕ{I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I1}V1, T⦄.
+/2 width=5 by fqu_flat_dx, fqup_strap1/ qed.
+
+lemma fqup_flat_dx_bind_dx: ∀a,I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.ⓑ{a,I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I2}V2, T⦄.
+/2 width=5 by fqu_bind_dx, fqup_strap1/ qed.
+
+(* Basic eliminators ********************************************************)
+
+lemma fqup_ind: ∀G1,L1,T1. ∀R:relation3 ….
+                (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+                (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃ ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
+                ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2.
+#G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
+@(tri_TC_ind … IH1 IH2 G2 L2 T2 H)
+qed-.
+
+lemma fqup_ind_dx: ∀G2,L2,T2. ∀R:relation3 ….
+                   (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → R G1 L1 T1) →
+                   (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃+ ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
+                   ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G1 L1 T1.
+#G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
+@(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H)
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fqup_fwd_fw: ∀G1,G2,L1,L2,T1,T2.
+                   ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}.
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+/3 width=3 by fqu_fwd_fw, transitive_lt/
+qed-.
+
+(* Advanced eliminators *****************************************************)
+
+lemma fqup_wf_ind: ∀R:relation3 …. (
+                      ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+                      ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → R G2 L2 T2
+                   ) → ∀G1,L1,T1. R G1 L1 T1.
+#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=7 by fqup_fwd_fw/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp_fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_fqup.ma
similarity index 93%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp_fsupp.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_fqup.ma
index a8422e6eb..a6bff5ede 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp_fsupp.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_fqup.ma
@@ -12,11 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/fsupp.ma".
+include "basic_2/substitution/fqup.ma".
 
 (* PLUS-ITERATED SUPCLOSURE *************************************************)
 
 (* Main propertis ***********************************************************)
 
-theorem fsupp_trans: tri_transitive … fsupp.
+theorem fqup_trans: tri_transitive … fqup.
 /2 width=5 by tri_TC_transitive/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma
new file mode 100644
index 000000000..ef5af3100
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma
@@ -0,0 +1,69 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/relations/suptermstar_6.ma".
+include "basic_2/relocation/fquq.ma".
+
+(* STAR-ITERATED SUPCLOSURE *************************************************)
+
+definition fqus: tri_relation genv lenv term ≝ tri_TC … fquq.
+
+interpretation "star-iterated structural successor (closure)"
+   'SupTermStar G1 L1 T1 G2 L2 T2 = (fqus G1 L1 T1 G2 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma fqus_ind: ∀G1,L1,T1. ∀R:relation3 …. R G1 L1 T1 →
+                (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃⸮ ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
+                ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G2 L2 T2.
+#G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
+@(tri_TC_star_ind … IH1 IH2 G2 L2 T2 H) //
+qed-.
+
+lemma fqus_ind_dx: ∀G2,L2,T2. ∀R:relation3 …. R G2 L2 T2 →
+                   (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
+                   ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G1 L1 T1.
+#G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
+@(tri_TC_star_ind_dx … IH1 IH2 G1 L1 T1 H) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma fqus_refl: tri_reflexive … fqus.
+/2 width=1 by tri_inj/ qed.
+
+lemma fquq_fqus: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
+/2 width=1 by tri_inj/ qed.
+
+lemma fqus_strap1: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                   ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
+/2 width=5 by tri_step/ qed.
+
+lemma fqus_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ →
+                   ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
+/2 width=5 by tri_TC_strap/ qed.
+
+lemma fqus_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ →
+                  ∀L1,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
+                  ⦃G1, L1, U1⦄ ⊃* ⦃G2, K2, T2⦄.
+#G1 #G2 #K1 #K2 #T1 #T2 #H @(fqus_ind … H) -G2 -K2 -T2
+/3 width=5 by fqus_strap1, fquq_fqus, fquq_drop/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fqus_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}.
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -L2 -T2
+/3 width=3 by fquq_fwd_fw, transitive_le/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups_fsups.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma
similarity index 93%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/fsups_fsups.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma
index fdee74619..295d45b17 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups_fsups.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma
@@ -12,11 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/fsups.ma".
+include "basic_2/substitution/fqus.ma".
 
 (* STAR-ITERATED SUPCLOSURE *************************************************)
 
 (* Main properties **********************************************************)
 
-theorem fsups_trans: tri_transitive … fsups.
+theorem fqus_trans: tri_transitive … fqus.
 /2 width=5 by tri_TC_transitive/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma
deleted file mode 100644
index 3c8da530a..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma
+++ /dev/null
@@ -1,102 +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/notation/relations/suptermplus_6.ma".
-include "basic_2/relocation/fsup.ma".
-
-(* PLUS-ITERATED SUPCLOSURE *************************************************)
-
-definition fsupp: tri_relation genv lenv term ≝ tri_TC … fsup.
-
-interpretation "plus-iterated structural successor (closure)"
-   'SupTermPlus G1 L1 T1 G2 L2 T2 = (fsupp G1 L1 T1 G2 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma fsup_fsupp: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
-/2 width=1 by tri_inj/ qed.
-
-lemma fsupp_strap1: ∀G1,G,G2,L1,L,L2,T1,T,T2.
-                    ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃ ⦃G2, L2, T2⦄ →
-                    ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
-/2 width=5 by tri_step/ qed.
-
-lemma fsupp_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2.
-                    ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃+ ⦃G2, L2, T2⦄ →
-                    ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
-/2 width=5 by tri_TC_strap/ qed.
-
-lemma fsupp_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
-                   ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ → ⦃G1, L1, U1⦄ ⊃+ ⦃G2, K2, T2⦄.
-#G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #e #HLK1 #HTU1 #HT12 elim (eq_or_gt … e) #H destruct
-[ >(ldrop_inv_O2 … HLK1) -L1 <(lift_inv_O2 … HTU1) -U1 //
-| /3 width=5 by fsupp_strap2, fsup_drop_lt/
-]
-qed-.
-
-lemma fsupp_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃+ ⦃G, K, V⦄.
-/3 width=6 by fsup_lref_O, fsup_fsupp, lift_lref_ge, fsupp_ldrop/ qed.
-
-lemma fsupp_pair_sn: ∀I,G,L,V,T. ⦃G, L, ②{I}V.T⦄ ⊃+ ⦃G, L, V⦄.
-/2 width=1 by fsup_pair_sn, fsup_fsupp/ qed.
-
-lemma fsupp_bind_dx: ∀a,I,G,L,V,T. ⦃G, L, ⓑ{a,I}V.T⦄ ⊃+ ⦃G, L.ⓑ{I}V, T⦄.
-/2 width=1 by fsup_bind_dx, fsup_fsupp/ qed.
-
-lemma fsupp_flat_dx: ∀I,G,L,V,T. ⦃G, L, ⓕ{I}V.T⦄ ⊃+ ⦃G, L, T⦄.
-/2 width=1 by fsup_flat_dx, fsup_fsupp/ qed.
-
-lemma fsupp_flat_dx_pair_sn: ∀I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.②{I2}V2.T⦄ ⊃+ ⦃G, L, V2⦄.
-/2 width=5 by fsup_pair_sn, fsupp_strap1/ qed.
-
-lemma fsupp_bind_dx_flat_dx: ∀a,G,I1,I2,L,V1,V2,T. ⦃G, L, ⓑ{a,I1}V1.ⓕ{I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I1}V1, T⦄.
-/2 width=5 by fsup_flat_dx, fsupp_strap1/ qed.
-
-lemma fsupp_flat_dx_bind_dx: ∀a,I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.ⓑ{a,I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I2}V2, T⦄.
-/2 width=5 by fsup_bind_dx, fsupp_strap1/ qed.
-
-(* Basic eliminators ********************************************************)
-
-lemma fsupp_ind: ∀G1,L1,T1. ∀R:relation3 ….
-                 (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                 (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃ ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
-                 ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2.
-#G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
-@(tri_TC_ind … IH1 IH2 G2 L2 T2 H)
-qed-.
-
-lemma fsupp_ind_dx: ∀G2,L2,T2. ∀R:relation3 ….
-                    (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → R G1 L1 T1) →
-                    (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃+ ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
-                    ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G1 L1 T1.
-#G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
-@(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H)
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma fsupp_fwd_fw: ∀G1,G2,L1,L2,T1,T2.
-                    ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}.
-#G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … H) -G2 -L2 -T2
-/3 width=3 by fsup_fwd_fw, transitive_lt/
-qed-.
-
-(* Advanced eliminators *****************************************************)
-
-lemma fsupp_wf_ind: ∀R:relation3 …. (
-                       ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                       ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → R G2 L2 T2
-                    ) → ∀G1,L1,T1. R G1 L1 T1.
-#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=7 by fsupp_fwd_fw/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma
deleted file mode 100644
index acc34d75c..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma
+++ /dev/null
@@ -1,69 +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/notation/relations/suptermstar_6.ma".
-include "basic_2/relocation/fsupq.ma".
-
-(* STAR-ITERATED SUPCLOSURE *************************************************)
-
-definition fsups: tri_relation genv lenv term ≝ tri_TC … fsupq.
-
-interpretation "star-iterated structural successor (closure)"
-   'SupTermStar G1 L1 T1 G2 L2 T2 = (fsups G1 L1 T1 G2 L2 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma fsups_ind: ∀G1,L1,T1. ∀R:relation3 …. R G1 L1 T1 →
-                 (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃⸮ ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
-                 ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G2 L2 T2.
-#G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
-@(tri_TC_star_ind … IH1 IH2 G2 L2 T2 H) //
-qed-.
-
-lemma fsups_ind_dx: ∀G2,L2,T2. ∀R:relation3 …. R G2 L2 T2 →
-                    (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
-                    ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G1 L1 T1.
-#G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
-@(tri_TC_star_ind_dx … IH1 IH2 G1 L1 T1 H) //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma fsups_refl: tri_reflexive … fsups.
-/2 width=1 by tri_inj/ qed.
-
-lemma fsupq_fsups: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
-/2 width=1 by tri_inj/ qed.
-
-lemma fsups_strap1: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                    ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
-/2 width=5 by tri_step/ qed.
-
-lemma fsups_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ →
-                    ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
-/2 width=5 by tri_TC_strap/ qed.
-
-lemma fsups_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ →
-                   ∀L1,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
-                   ⦃G1, L1, U1⦄ ⊃* ⦃G2, K2, T2⦄.
-#G1 #G2 #K1 #K2 #T1 #T2 #H @(fsups_ind … H) -G2 -K2 -T2
-/3 width=5 by fsups_strap1, fsupq_fsups, fsupq_drop/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma fsups_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}.
-#G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2
-/3 width=3 by fsupq_fwd_fw, transitive_le/
-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 c5f04455d..c43385009 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -203,8 +203,8 @@ table {
           }
         ]
         [ { "iterated structural successor for closures" * } {
-             [ "fsups ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fsups_fsups" * ]
-             [ "fsupp ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fsupp_fsupp" * ]
+             [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_fqus" * ]
+             [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ]
           }
         ]
         [ { "generic local env. slicing" * } {
@@ -225,7 +225,7 @@ table {
    class "orange"
    [ { "relocation" * } {
         [ { "structural successor for closures" * } {
-             [ "fsup ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fsupq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fsupq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ]
+             [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ]
           }
         ]
         [ { "global env. slicing" * } {
-- 
2.39.2