2 lemma lfxss_zero: ∀R,I,L1,L2,V1. L1 ⦻**[R, V1] L2 → ∀V2.
3 R L1 V1 V2 → L1.ⓑ{I}V1 ⦻**[R, #0] L2.ⓑ{I}V2.
6 elim H -L2 /3 width=5 by lfxs_zero, inj/
7 #L #L2 #H0 #HL2 #IH #V2 #HV12
8 lapply (IH … HV12) -IH #HL1
9 @(step … HL1) -HL1 @lfxs_zero
11 axiom pippo_fwd: ∀R,I,Y1,L2,V2,T. Y1 ⦻*[R, T] L2.ⓑ{I}V2 →
12 ∃∃L1,V1. Y1 = L1.ⓑ{I}V1.
14 fact pippo: ∀R,I,L1,Y,T,V. L1.ⓑ{I}V ⦻**[R, T] Y →
15 ∀L2,V1. Y = L2.ⓑ{I}V1 →
17 L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V2.
18 #R #I #L1 #Y #T #V #H elim H -Y
19 [ /3 width=2 by lfxs_pair_repl_dx, inj/
20 | #L #Y #_ #HL2 #IH #L2 #V1 #H #V2 #HV2 destruct
21 elim (pippo_fwd … HL2) #L0 #V0 #H destruct
22 @step [2: @(IH … HV2) // | skip ] -IH -HV2
24 lemma lfxss_pair_repl_dx: ∀R,I,L1,L2,T,V,V1.
25 L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V1 →
27 L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V2.
28 #R #I #L1 #L2 #T #V #V1 * #f #Hf #HL12 #V2 #HR
29 /3 width=5 by lexs_pair_repl, ex2_intro/