- [ lapply (isuni_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH
- lapply (after_isid_inv_dx … Hg … Hg2) -Hg #Hg
- /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, liftsb_eq_repl_back, isid_push, ex2_intro/
- | lapply (isuni_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HI1
+ [ lapply (pr_isu_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH
+ lapply (pr_after_isi_inv_dx … Hg … Hg2) -Hg #Hg
+ /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, liftsb_eq_repl_back, pr_isi_push, ex2_intro/
+ | lapply (pr_isu_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HI1