Let J, le and net be given.

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

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

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

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

Use reflexivity.

∎