#g * -g
#f #g #Hf * /2 width=3 by ex2_intro/
qed-.
(* Advanced inversion lemmas ************************************************)
#g * -g
#f #g #Hf * /2 width=3 by ex2_intro/
qed-.
(* Advanced inversion lemmas ************************************************)
#g #H elim (isid_inv_gen … H) -H
#f #Hf * -g #g #H elim (discr_next_push … H)
qed-.
(* Main inversion lemmas ****************************************************)
#g #H elim (isid_inv_gen … H) -H
#f #Hf * -g #g #H elim (discr_next_push … H)
qed-.
(* Main inversion lemmas ****************************************************)
#n elim n -n /3 width=3 by isid_push/
qed.
(* Inversion lemmas with iterated push **************************************)
#n elim n -n /3 width=3 by isid_push/
qed.
(* Inversion lemmas with iterated push **************************************)
#n elim n -n /3 width=3 by isid_inv_push/
qed.
(* Properties with tail *****************************************************)
#n elim n -n /3 width=3 by isid_inv_push/
qed.
(* Properties with tail *****************************************************)
#f cases (pn_split f) * #g * -f #H
[ /2 width=3 by isid_inv_push/
| elim (isid_inv_next … H) -H //
#f cases (pn_split f) * #g * -f #H
[ /2 width=3 by isid_inv_push/
| elim (isid_inv_next … H) -H //