final na,e for big-tree rediction and computation

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / ygt_ygt.ma

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 5910f81cadea11167921b88f03641d8720eb551e..98fd435a3e37a10b0917badc4c5f9de8225cecc7 100644 (file)
--- 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-.