]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / notes.txt
1 lemma pr_pat_after_uni_tls (i2) (i1):
2       ∀f2. @❨i1, f2❩ ≘ i2 →
3       ∀f. 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
4
5 . replace.sh . "/substitution/" "/unwind/"
6 . replace.sh . ↑ ▼ 
7
8 266D;MUSIC FLAT SIGN;So;0;ON;;;;;N;FLAT;;;;
9 266E;MUSIC NATURAL SIGN;So;0;ON;;;;;N;NATURAL;;;;
10 266F;MUSIC SHARP SIGN;Sm;0;ON;;;;;N;SHARP;;;;