X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fs_computation%2Ffqup.ma;h=e3dae5bf4c4393f7de655c5bdd21283207681e40;hp=51c5afc6a10cd5a244234c5150aae88f8f96fb3e;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hpb=d71e53021b0c17e1a00c2d623e7139c6d18069d5

diff --git a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma
index 51c5afc6a..e3dae5bf4 100644
--- a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma
@@ -83,4 +83,10 @@ lemma fqup_ind_dx: ∀b,G2,L2,T2. ∀Q:relation3 ….
 @(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H)
 qed-.
 
+(* Advanced properties ******************************************************)
+
+lemma fqup_zeta (b) (p) (I) (G) (K) (V):
+                ∀T1,T2. ⬆*[1]T2 ≘ T1 → ⦃G,K,ⓑ{p,I}V.T1⦄ ⊐+[b] ⦃G,K,T2⦄.
+/4 width=5 by fqup_strap2, fqu_fqup, fqu_drop/ qed.
+
 (* Basic_2A1: removed theorems 1: fqup_drop *)