matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc

   1 lemma pippo (f):
   2       f@❨𝟏❩⨮⇂f = f.
   3 * #p #f //
   4 qed.
   5
   6 axiom pippo2 (f) (p):
   7       f@❨p❩ + (⇂*[ninj p]f)@❨𝟏❩ = f@❨↑p❩.
   8
   9 lemma tr_uni_tl (n):
  10       (𝐢) = ⇂𝐮❨n❩.
  11 // qed.
  12
  13 axiom tr_uni_tls_pos (p:pnat) (n):
  14       (𝐢) = ⇂*[p]𝐮❨n❩.
  15 (*
  16 #p #n
  17 >nsucc_pnpred <stream_tls_swap
  18 <tr_uni_tl <tr_id_tls
  19 // qed.
  20 *)
  21