matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_lfxs.etc

   1 theorem lfxs_trans: ∀R. lexs_frees_confluent R cfull →
   2                     ∀T. Transitive … (lfxs R T).
   3 #R #H1R #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2
   4 elim (H1R … Hf1 … HL1) #f #H0 #H1
   5 lapply (frees_mono … Hf2 … H0) -Hf2 -H0 #Hf2
   6 lapply (lexs_eq_repl_back … HL2 … Hf2) -f2 #HL2
   7 lapply (sle_lexs_trans … HL1 … H1) -HL1 // #Hl1
   8 @(ex2_intro … f)
   9
  10 /4 width=7 by lreq_trans, lexs_eq_repl_back, ex2_intro/
  11 qed-.