Let J, le and net be given.
We will prove ((net_pack J le net) 1) 0 = le.
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_0_eq le net) (from left to right).
Use reflexivity.
∎