passive support for global environments completed!

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma
index 99deeefb1c2e71cf9bcfc8255d3cbe2228796630..443dbcbf0f8f7933c11e3591321f1cdd7dd1f01c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma
@@ -18,5 +18,5 @@ include "basic_2/dynamic/ygt.ma".
 
 (* Main properties **********************************************************)
 
-theorem ygt_trans: ∀h,g. bi_transitive … (ygt h g).
-/3 width=4 by ygt_fwd_yprs, ygt_yprs_trans/ qed-.
+theorem ygt_trans: ∀h,g. tri_transitive … (ygt h g).
+/3 width=5 by ygt_fwd_yprs, ygt_yprs_trans/ qed-.