X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fs_computation%2Ffqup.ma;h=a30e03a457e15b476628f30dd6fe1bcea864f5ad;hp=5f14e8cec84911cf1af36a464d0106995ee44e65;hb=5c186c72f508da0849058afeecc6877cd9ed6303;hpb=282511a928532676813d99d08594cd5f98fcb80e

diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma
index 5f14e8cec..a30e03a45 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma
@@ -67,19 +67,19 @@ lemma fqup_flat_dx_bind_dx: ∀b,p,I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.ⓑ{p,I
 
 (* Basic eliminators ********************************************************)
 
-lemma fqup_ind: ∀b,G1,L1,T1. ∀R:relation3 ….
-                (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
-                ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G2 L2 T2.
-#b #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
+lemma fqup_ind: ∀b,G1,L1,T1. ∀Q:relation3 ….
+                (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+                (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G L T → Q G2 L2 T2) →
+                ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2.
+#b #G1 #L1 #T1 #Q #IH1 #IH2 #G2 #L2 #T2 #H
 @(tri_TC_ind … IH1 IH2 G2 L2 T2 H)
 qed-.
 
-lemma fqup_ind_dx: ∀b,G2,L2,T2. ∀R:relation3 ….
-                   (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G1 L1 T1) →
-                   (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
-                   ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G1 L1 T1.
-#b #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
+lemma fqup_ind_dx: ∀b,G2,L2,T2. ∀Q:relation3 ….
+                   (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G1 L1 T1) →
+                   (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G L T → Q G1 L1 T1) →
+                   ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G1 L1 T1.
+#b #G2 #L2 #T2 #Q #IH1 #IH2 #G1 #L1 #T1 #H
 @(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H)
 qed-.