severe bug found in parallel zeta

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / s_computation / fqup.ma

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 51c5afc6a10cd5a244234c5150aae88f8f96fb3e..e3dae5bf4c4393f7de655c5bdd21283207681e40 100644 (file)
--- 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 *)