matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_lreq.etc

   1 fact lreq_lpxs_trans_lleq_aux: ∀h,o,G,L1,L0,l,k. L1 ⩬[l, k] L0 → k = ∞ →
   2                                ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 →
   3                                ∃∃L. L ⩬[l, k] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L &
   4                                     (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L).
   5 #h #o #G #L1 #L0 #l #k #H elim H -L1 -L0 -l -k
   6 [ #l #k #_ #L2 #H >(lpxs_inv_atom1 … H) -H
   7   /3 width=5 by ex3_intro, conj/
   8 | #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #Hm destruct
   9 | #I #L1 #L0 #V1 #k #HL10 #IHL10 #Hm #Y #H
  10   elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
  11   lapply (ysucc_inv_Y_dx … Hm) -Hm #Hm
  12   elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
  13   @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, lreq_cpxs_trans, lreq_pair/
  14   #T elim (IH T) #HL0dx #HL0sn
  15   @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_pair_O_Y/
  16 | #I1 #I0 #L1 #L0 #V1 #V0 #l #k #HL10 #IHL10 #Hm #Y #H
  17   elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
  18   elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
  19   @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, lreq_succ/
  20   #T elim (IH T) #HL0dx #HL0sn
  21   @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_succ/
  22 ]
  23 qed-.
  24
  25 lemma lreq_lpxs_trans_lleq: ∀h,o,G,L1,L0,l. L1 ⩬[l, ∞] L0 →
  26                             ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 →
  27                             ∃∃L. L ⩬[l, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L &
  28                                  (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L).
  29 /2 width=1 by lreq_lpxs_trans_lleq_aux/ qed-.