(*** after_uni_dx *)
lemma pr_after_nat_uni (l2) (l1):
- â\88\80f2. @â\86\91â\9dªl1, f2â\9d« ≘ l2 →
+ â\88\80f2. @â\86\91â\9d¨l1, f2â\9d© ≘ l2 →
∀f. f2 ⊚ 𝐮❨l1❩ ≘ f → 𝐮❨l2❩ ⊚ ⫰*[l2] f2 ≘ f.
#l2 @(nat_ind_succ … l2) -l2
[ #l1 #f2 #Hf2 #f #Hf
(*** after_uni_sn *)
lemma pr_nat_after_uni_tls (l2) (l1):
- â\88\80f2. @â\86\91â\9dªl1, f2â\9d« ≘ l2 →
+ â\88\80f2. @â\86\91â\9d¨l1, f2â\9d© ≘ l2 →
∀f. 𝐮❨l2❩ ⊚ ⫰*[l2] f2 ≘ f → f2 ⊚ 𝐮❨l1❩ ≘ f.
#l2 @(nat_ind_succ … l2) -l2
[ #l1 #f2 #Hf2 #f #Hf