Let J, le and net be given.

We will prove (net_pack J le net) 0 = J.

rewrite the current goal using (net_pack_def J le net) (from left to right).

rewrite the current goal using (tuple_2_0_eq J (le,net)) (from left to right).

Use reflexivity.

∎