#f1 #f * -f1 -f
#f1 #f #g1 #g #Hf1 #H1 #H #f2 #Hf2
[ cases (eq_inv_px … Hf2 … H) | cases (eq_inv_nx … Hf2 … H) ] -g
/3 width=5 by eq_push, eq_next/
qed-.
#f1 #f * -f1 -f
#f1 #f #g1 #g #Hf1 #H1 #H #f2 #Hf2
[ cases (eq_inv_px … Hf2 … H) | cases (eq_inv_nx … Hf2 … H) ] -g
/3 width=5 by eq_push, eq_next/
qed-.