#f #n elim n -n /2 width=5 by at_inv_npx/
#n #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
#j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
#i2 #Hi * -j2 /2 width=3 by ex2_intro/
qed-.
#f #n elim n -n /2 width=5 by at_inv_npx/
#n #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
#j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
#i2 #Hi * -j2 /2 width=3 by ex2_intro/
qed-.