#f #H elim H -f /3 width=2 by uni_isid, ex_intro/
#f #_ #g #H * /3 width=6 by eq_next, ex_intro/
qed-.
(* Inversion lemmas with test for uniformity ********************************)
#f #H elim H -f /3 width=2 by uni_isid, ex_intro/
#f #_ #g #H * /3 width=6 by eq_next, ex_intro/
qed-.
(* Inversion lemmas with test for uniformity ********************************)