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 0c2ae2995fe4de7e45ce44686deffd67db045f7d..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
@@ -16,5 +16,7 @@ include "basic_2/computation/ygt.ma".
 
 (* "BIG TREE" ORDER FOR CLOSURES ********************************************)
 
-theorem ygt_trans: ∀h,g. bi_transitive … (ygt h g).
-/2 width=4/ qed-.
+(* Main properties **********************************************************)
+
+theorem ygt_trans: ∀h,g. tri_transitive … (ygt h g).
+/3 width=5 by ygt_fwd_fpbs, ygt_fpbs_trans/ qed-.