#f1 #f2 #x #y * -f1 -f2 -x
#f1 #f2 #x #g1 [1,2: #g2 ] #g #Hx #H1 [1,2: #H2 ] #H0x #Hy
[ cases (pr_after_inv_push_bi … Hy … H1 H2) -g1 -g2 /3 width=8 by pr_eq_push/
#f1 #f2 #x #y * -f1 -f2 -x
#f1 #f2 #x #g1 [1,2: #g2 ] #g #Hx #H1 [1,2: #H2 ] #H0x #Hy
[ cases (pr_after_inv_push_bi … Hy … H1 H2) -g1 -g2 /3 width=8 by pr_eq_push/