X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Freqg.ma;h=93f10a93d4a2359ea0b16e54243cff51b75ea663;hp=1c5d5ed9074426338777e671831f42b7d0ed6f8f;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hpb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqg.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqg.ma
index 1c5d5ed90..93f10a93d 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/reqg.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/reqg.ma
@@ -59,10 +59,10 @@ lemma frees_teqg_conf_seqg (S):
   >(teqg_inv_gref1 … H1) -X /2 width=1 by frees_gref/
 | #f1V #f1T #f1 #p #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1
   elim (teqg_inv_pair1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct
-  /6 width=5 by frees_bind, sex_inv_tl, ext2_pair, sle_sex_trans, sor_inv_sle_dx, sor_inv_sle_sn/
+  /6 width=5 by frees_bind, sex_inv_tl, ext2_pair, sle_sex_trans, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn/
 | #f1V #f1T #f1 #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1
   elim (teqg_inv_pair1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct
-  /5 width=5 by frees_flat, sle_sex_trans, sor_inv_sle_dx, sor_inv_sle_sn/
+  /5 width=5 by frees_flat, sle_sex_trans, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn/
 ]
 qed-.