[ /3 width=2 by frees_inv_atom, isid_inv_eq_repl/
| /4 width=5 by frees_inv_sort, eq_push_inv_isid, isid_inv_eq_repl, eq_trans/
[ /3 width=2 by frees_inv_atom, isid_inv_eq_repl/
| /4 width=5 by frees_inv_sort, eq_push_inv_isid, isid_inv_eq_repl, eq_trans/