lemma lpair_ltail: ∀L,I,V. ∃∃J,K,W. L.ⓑ{I}V = ⓑ{J}W.K & |L| = |K|.
#L elim L -L /2 width=5 by ex2_3_intro/
#L #Z #X #IHL #I #V elim (IHL Z X) -IHL
lemma lpair_ltail: ∀L,I,V. ∃∃J,K,W. L.ⓑ{I}V = ⓑ{J}W.K & |L| = |K|.
#L elim L -L /2 width=5 by ex2_3_intro/
#L #Z #X #IHL #I #V elim (IHL Z X) -IHL