X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fygt_ygt.ma;h=98fd435a3e37a10b0917badc4c5f9de8225cecc7;hb=f5cd5870668ed096f6d93b005e2acd3bd555f3b0;hp=5910f81cadea11167921b88f03641d8720eb551e;hpb=f5c6d4c41cbbdabdf998be0c4a8242849a790f1b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma
index 5910f81ca..98fd435a3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma
@@ -19,4 +19,4 @@ include "basic_2/computation/ygt.ma".
 (* Main properties **********************************************************)
 
 theorem ygt_trans: ∀h,g. tri_transitive … (ygt h g).
-/3 width=5 by ygt_fwd_yprs, ygt_yprs_trans/ qed-.
+/3 width=5 by ygt_fwd_fpbs, ygt_fpbs_trans/ qed-.