-theorem lexs_meet: ∀RN,RP,L1,L2,f1. L1 ⦻*[RN, RP, f1] L2 →
- ∀f2. L1 ⦻*[RN, RP, f2] L2 →
- ∀f. f1 ⋒ f2 ≡ f → L1 ⦻*[RN, RP, f] L2.
-#RN #RP #L1 #L2 #f1 #H elim H -L1 -L2 -f1 //
-#I #L1 #L2 #V1 #V2 #f1 #_ #H1V #IH #f2 elim (pn_split f2) *
-#g2 #H #H2 #f #Hf destruct
-[1,3: elim (lexs_inv_push … H2) |2,4: elim (lexs_inv_next … H2) ] -H2
-#H2 #H2V #_
-[ elim (sand_inv_npx … Hf) | elim (sand_inv_ppx … Hf) | elim (sand_inv_nnx … Hf) | elim (sand_inv_pnx … Hf) ] -Hf
-/3 width=5 by lexs_next, lexs_push/
+lemma lexs_meet: ∀RN,RP,L1,L2.
+ ∀f1. L1 ⦻*[RN, RP, f1] L2 →
+ ∀f2. L1 ⦻*[RN, RP, f2] L2 →
+ ∀f. f1 ⋒ f2 ≡ f → L1 ⦻*[RN, RP, f] L2.
+#RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 //
+#f1 #I #L1 #L2 #V1 #V2 #_ #HV12 #IH #f2 #H #f #Hf
+elim (pn_split f2) * #g2 #H2 destruct
+try elim (lexs_inv_push … H) try elim (lexs_inv_next … H) -H
+[ elim (sand_inv_npx … Hf) | elim (sand_inv_nnx … Hf)
+| elim (sand_inv_ppx … Hf) | elim (sand_inv_pnx … Hf)
+] -Hf /3 width=5 by lexs_next, lexs_push/