matita/matita/contribs/lambdadelta/delayed_updating/notes.txt

   1 1) (⫯f)@(1) = 1
   2 2) f@❨d-n❩ = k → n <= d → (f∘𝐮❨n❩)@❨d❩ = k
   3 3) f@❨d-1❩ = k-1 → 1 < d → 1 < k → (⫯f)@❨d❩ = k
   4
   5
   6 lemma pr_pat_after_uni_tls (i2) (i1):
   7       ∀f2. @❨i1, f2❩ ≘ i2 →
   8       ∀f. 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
   9
  10 . replace.sh . "/substitution/" "/unwind/"
  11 . replace.sh . ↑ ▼