update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / lfxs_lex.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lex.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lex.etc
new file mode 100644 (file)
index 0000000..6303d64
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lex.etc
@@ -0,0 +1,12 @@
+(* Note: this is the companion of lfxs_trans_fsle *)
+theorem lfxs_trans_fsge: ∀R,R1,R2,R3.
+                         lfxs_transitive_next R1 R R3 →
+                         ∀L1,L,T. L1 ⪤*[R1, T] L →
+                         ∀L2. L ⪤[R2] L2 → L1 ⪤*[R3, T] L2.
+#R #R1 #R2 #R3 #HR #L1 #L #T #H
+cases H -H #f1 #Hf1 #HL1 #L2 * #f #Hf #HL2
+@(ex2_intro … Hf1) -Hf1
+@(lexs_trans_gen … HL1) -HL1
+[5: @(sle_lexs_conf … HL2) -HL2 /2 width=1 by sle_isid_sn/ |1,2: skip
+|4: //
+|3: