(*** coafter_fwd_pushs *)
lemma pr_coafter_des_pushs_dx (n) (m):
- â\88\80g2,f1,g. g2 ~â\8a\9a ⫯*[m]f1 â\89\98 g â\86\92 @â\86\91â\9dªm, g2â\9d« ≘ n →
+ â\88\80g2,f1,g. g2 ~â\8a\9a ⫯*[m]f1 â\89\98 g â\86\92 @â\86\91â\9d¨m, g2â\9d© ≘ n →
∃∃f. ⫰*[n]g2 ~⊚ f1 ≘ f & ⫯*[n] f = g.
#n @(nat_ind_succ … n) -n
[ #m #g2 #f1 #g #Hg #H