X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Flfpr.ma;h=61fc781b245d0eb0808743edaf7252470b1959b4;hb=b8e20d61b2e76f7a36f05b8803e60cc3388c0882;hp=381233f0436b84ca59d2362a86bb43e40b00bf65;hpb=98d4ee8a0212abae10cee962f7f81f658b70f611;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma
index 381233f04..61fc781b2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma
@@ -151,12 +151,13 @@ lemma lfpr_fwd_pair_sn: ∀h,I,G,L1,L2,V,T.
                         ⦃G, L1⦄ ⊢ ➡[h, ②{I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡[h, V] L2.
 /2 width=3 by lfxs_fwd_pair_sn/ qed-.
 
-(* Basic_2A1: removed theorems 14:
+(* Basic_2A1: removed theorems 16:
               lpr_inv_atom1 lpr_inv_pair1 lpr_inv_atom2 lpr_inv_pair2
               lpr_refl lpr_pair
               lpr_fwd_length lpr_lpx
               lpr_drop_conf drop_lpr_trans lpr_drop_trans_O1
               cpr_conf_lpr lpr_cpr_conf_dx lpr_cpr_conf_sn
+              fqu_lpr_trans fquq_lpr_trans
 *)
 (* Basic_1: removed theorems 7:
             wcpr0_gen_sort wcpr0_gen_head