[2: >length_append normalize in ⊢ (??(??%)); // ]
#q #r #M #Hq #HM1 #HM
lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr
@(ex3_2_intro … HM1) -M1 // -q
@(dst_step_sn … HM) /2 width=1/
| #p #_ #IHp #N1 #N2 #H1 #M1 #H2
[2: >length_append normalize in ⊢ (??(??%)); // ]
#q #r #M #Hq #HM1 #HM
lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr
@(ex3_2_intro … HM1) -M1 // -q
@(dst_step_sn … HM) /2 width=1/
| #p #_ #IHp #N1 #N2 #H1 #M1 #H2