matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lex.etc

   1 (* Note: this is the companion of lfxs_trans_fsle *)
   2 theorem lfxs_trans_fsge: ∀R,R1,R2,R3.
   3                          lfxs_transitive_next R1 R R3 →
   4                          ∀L1,L,T. L1 ⪤*[R1, T] L →
   5                          ∀L2. L ⪤[R2] L2 → L1 ⪤*[R3, T] L2.
   6 #R #R1 #R2 #R3 #HR #L1 #L #T #H
   7 cases H -H #f1 #Hf1 #HL1 #L2 * #f #Hf #HL2
   8 @(ex2_intro … Hf1) -Hf1
   9 @(lexs_trans_gen … HL1) -HL1
  10 [5: @(sle_lexs_conf … HL2) -HL2 /2 width=1 by sle_isid_sn/ |1,2: skip
  11 |4: //
  12 |3: