matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss_etc.ma

   1 (*
   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.
   4 #R #I #L1 #L2 #V1 #H
   5
   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
  10
  11 axiom pippo_fwd: ∀R,I,Y1,L2,V2,T. Y1 ⦻*[R, T] L2.ⓑ{I}V2 →
  12                  ∃∃L1,V1. Y1 = L1.ⓑ{I}V1.
  13
  14 fact pippo: ∀R,I,L1,Y,T,V. L1.ⓑ{I}V ⦻**[R, T] Y →
  15             ∀L2,V1. Y = L2.ⓑ{I}V1 →
  16             ∀V2. R L1 V V2 →
  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
  23
  24 lemma lfxss_pair_repl_dx: ∀R,I,L1,L2,T,V,V1.
  25                           L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V1 →
  26                           ∀V2. R L1 V V2 →
  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/
  30 qed-.
  31 *)