matita/matita/contribs/lambdadelta/basic_2/etc/lveq.etc

   1 fact lveq_inv_pair_bind_aux: ∀L1,L2,n1,n2. L1 ≋ ⓧ*[n1, n2] L2 →
   2                              ∀I1,I2,K1,K2,V1. K1.ⓑ{I1}V1 = L1 → K2.ⓘ{I2} = L2 →
   3                              ∨∨ ∃∃m. K1 ≋ ⓧ*[m, m] K2 & 0 = n1 & 0 = n2
   4                               | ∃∃m1,m2. K1 ≋ ⓧ*[m1, m2] K2 &
   5                                          BUnit Void = I2 & ⫯m2 = n2.
   6 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
   7 [ #J1 #J2 #L1 #L2 #V1 #H1 #H2 destruct
   8 |2,3: #I1 #I2 #K1 #K2 #V #n #HK #_ #J1 #J2 #L1 #L2 #V1 #H1 #H2 destruct /3 width=2 by or_introl, ex3_intro/
   9 |4,5: #K1 #K2 #n1 #n2 #HK #IH #J1 #J2 #L1 #L2 #V1 #H1 #H2 destruct
  10  /3 width=4 by _/
  11 ]
  12 qed-.
  13
  14 lemma voids_inv_pair_bind: ∀I1,I2,K1,K2,V1,n1,n2. ⓧ*[n1]K1.ⓑ{I1}V1 ≋ ⓧ*[n2]K2.ⓘ{I2} →
  15                            ∨∨ ∃∃n. ⓧ*[n]K1 ≋ ⓧ*[n]K2 & 0 = n1 & 0 = n2
  16                             | ∃∃m2. ⓧ*[n1]K1.ⓑ{I1}V1 ≋ ⓧ*[m2]K2 &
  17                                     BUnit Void = I2 & ⫯m2 = n2.
  18 /2 width=5 by voids_inv_pair_bind_aux/ qed-.
  19
  20 fact voids_inv_bind_pair_aux: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
  21                               ∀I1,I2,K1,K2,V2. K1.ⓘ{I1} = L1 → K2.ⓑ{I2}V2 = L2 →
  22                               ∨∨ ∃∃n. ⓧ*[n]K1 ≋ ⓧ*[n]K2 & 0 = n1 & 0 = n2
  23                                | ∃∃m1. ⓧ*[m1]K1 ≋ ⓧ*[n2]K2.ⓑ{I2}V2 &
  24                                        BUnit Void = I1 & ⫯m1 = n1.
  25 #L1 #L2 #n1 #n2 * -L1 -L2 -n1 -n2
  26 [ #J1 #J2 #L1 #L2 #V1 #H1 #H2 destruct
  27 |2,3: #I1 #I2 #K1 #K2 #V #n #HK #J1 #J2 #L1 #L2 #V2 #H1 #H2 destruct /3 width=2 by or_introl, ex3_intro/
  28 |4,5: #K1 #K2 #n1 #n2 #HK #J1 #J2 #L1 #L2 #V2 #H1 #H2 destruct /3 width=3 by or_intror, ex3_intro/
  29 ]
  30 qed-.
  31
  32 lemma voids_inv_bind_pair: ∀I1,I2,K1,K2,V2,n1,n2. ⓧ*[n1]K1.ⓘ{I1} ≋ ⓧ*[n2]K2.ⓑ{I2}V2 →
  33                            ∨∨ ∃∃n. ⓧ*[n]K1 ≋ ⓧ*[n]K2 & 0 = n1 & 0 = n2
  34                             | ∃∃m1. ⓧ*[m1]K1 ≋ ⓧ*[n2]K2.ⓑ{I2}V2 &
  35                                     BUnit Void = I1 & ⫯m1 = n1.
  36 /2 width=5 by voids_inv_bind_pair_aux/ qed-.