X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfxs_lfxs.ma;h=654ab4d0da89625d9968dfe3981f733d31170275;hb=b4b5f03ffca4f250a1dc02f277b70e4f33ac8a9b;hp=26289760bd6072eddb473062f455c647cd2a6419;hpb=09b4420070d6a71990e16211e499b51dbb0742cb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
index 26289760b..654ab4d0d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
@@ -35,7 +35,19 @@ theorem lfxs_flat: ∀R,I,L1,L2,V,T.
 #R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2)
 /3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/
 qed.
+(*
+theorem lfxs_trans: ∀R. lexs_frees_confluent R cfull →
+                    ∀T. Transitive … (lfxs R T).
+#R #H1R #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2
+elim (H1R … Hf1 … HL1) #f #H0 #H1
+lapply (frees_mono … Hf2 … H0) -Hf2 -H0 #Hf2
+lapply (lexs_eq_repl_back … HL2 … Hf2) -f2 #HL2
+lapply (sle_lexs_trans … HL1 … H1) -HL1 // #Hl1
+@(ex2_intro … f)
 
+/4 width=7 by lreq_trans, lexs_eq_repl_back, ex2_intro/
+qed-.
+*)
 theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull →
                    R_confluent2_lfxs R R R R →
                    ∀T. confluent … (lfxs R T).