include "ground/relocation/gr_nat.ma".
include "ground/relocation/gr_coafter.ma".
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
-(* Forward lemmas with nat and iterated tail and pushs ************************************************)
+(* Destructions with gr_nat and gr_tls and gr_pushs *************************)
(*** coafter_fwd_pushs *)
lemma gr_coafter_des_pushs_dx (n) (m):
∀g2,f1,g. g2 ~⊚ ⫯*[m]f1 ≘ g → @↑❪m, g2❫ ≘ n →
- â\88\83â\88\83f. ⫱*[n]g2 ~⊚ f1 ≘ f & ⫯*[n] f = g.
+ â\88\83â\88\83f. â«°*[n]g2 ~⊚ f1 ≘ f & ⫯*[n] f = g.
#n @(nat_ind_succ … n) -n
[ #m #g2 #f1 #g #Hg #H
elim (gr_nat_inv_zero_dx … H) -H [|*: // ] #f2 #H1 #H2 destruct