(*** after_uni_succ_dx *)
lemma pr_after_pat_uni (i2) (i1):
- â\88\80f2. @â\9dªi1, f2â\9d« ≘ i2 →
+ â\88\80f2. @â\9d¨i1, f2â\9d© ≘ i2 →
∀f. f2 ⊚ 𝐮❨i1❩ ≘ f → 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f.
#i2 elim i2 -i2
[ #i1 #f2 #Hf2 #f #Hf
(*** after_uni_succ_sn *)
lemma pr_pat_after_uni_tls (i2) (i1):
- â\88\80f2. @â\9dªi1, f2â\9d« ≘ i2 →
+ â\88\80f2. @â\9d¨i1, f2â\9d© ≘ i2 →
∀f. 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
#i2 elim i2 -i2
[ #i1 #f2 #Hf2 #f #Hf