#RR #RS #RP #H1RP #H2RP #G #L1 #T @(fqup_wf_ind_eq (Ⓣ) … G L1 T) -G -L1 -T
#Z #Y #X #IH #G #L1 * [ * | * [ #p ] * ]
[ #s #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
lapply (aaa_inv_sort … HA) -HA #H destruct
>(lifts_inv_sort1 … H0) -H0
lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom
#RR #RS #RP #H1RP #H2RP #G #L1 #T @(fqup_wf_ind_eq (Ⓣ) … G L1 T) -G -L1 -T
#Z #Y #X #IH #G #L1 * [ * | * [ #p ] * ]
[ #s #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
lapply (aaa_inv_sort … HA) -HA #H destruct
>(lifts_inv_sort1 … H0) -H0
lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom