X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flprs_cprs.ma;h=1bcb46d37e387513b586c24bdd4960c5febfd496;hb=f282b35b958c9602fb1f47e5677b5805a046ac76;hp=9ce393c437959f4b71cba1de7b690709f878dacd;hpb=cb5ca7ea4e826e9331eabeaea44353caab00071e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma
index 9ce393c43..1bcb46d37 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma
@@ -35,6 +35,17 @@ lemma lprs_inv_pair2: ∀I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡* K2.ⓑ{I}V2 →
                                L1 = K1.ⓑ{I}V1.
 /3 width=3 by TC_lpx_sn_inv_pair2, lpr_cprs_trans/ qed-.
 
+(* Advanced eliminators *****************************************************)
+
+lemma lprs_ind_alt: ∀G. ∀R:relation lenv.
+                    R (⋆) (⋆) → (
+                       ∀I,K1,K2,V1,V2.
+                       ⦃G, K1⦄ ⊢ ➡* K2 → ⦃G, K1⦄ ⊢ V1 ➡* V2 →
+                       R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+                    ) →
+                    ∀L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → R L1 L2.
+/3 width=4 by TC_lpx_sn_ind, lpr_cprs_trans/ qed-.
+
 (* Properties on context-sensitive parallel computation for terms ***********)
 
 lemma lprs_cpr_trans: ∀G. s_r_transitive … (cpr G) (λ_. lprs G).