matita/matita/contribs/lambdadelta/basic_2/etc_new/lifts/lifts.etc

   1 (* Basic_1: was: lift_r *)
   2 lemma lift_refl: ∀T,l. ⬆[l, 0] T ≡ T.
   3 #T elim T -T
   4 [ * #i // #l elim (lt_or_ge i l) /2 width=1 by lift_lref_lt,
   5 lift_lref_ge/
   6 | * /2 width=1 by lift_bind, lift_flat/
   7 ]
   8 qed.
   9
  10 lemma lift_total: ∀T1,l,m. ∃T2. ⬆[l,m] T1 ≡ T2.
  11 #T1 elim T1 -T1
  12 [ * #i /2 width=2 by lift_sort, lift_gref, ex_intro/
  13   #l #m elim (lt_or_ge i l) /3 width=2 by lift_lref_lt, lift_lref_ge,
  14 ex_intro/
  15 | * [ #a ] #I #V1 #T1 #IHV1 #IHT1 #l #m
  16   elim (IHV1 l m) -IHV1 #V2 #HV12
  17   [ elim (IHT1 (l+1) m) -IHT1 /3 width=2 by lift_bind, ex_intro/
  18   | elim (IHT1 l m) -IHT1 /3 width=2 by lift_flat, ex_intro/
  19   ]
  20 ]
  21 qed.
  22
  23 lemma liftv_total: ∀l,m. ∀T1s:list term. ∃T2s. ⬆[l, m] T1s ≡ T2s.
  24 #l #m #T1s elim T1s -T1s
  25 [ /2 width=2 by liftv_nil, ex_intro/
  26 | #T1 #T1s * #T2s #HT12s
  27   elim (lift_total T1 l m) /3 width=2 by liftv_cons, ex_intro/
  28 ]
  29 qed-.