-(* Basic_1: was just: chead_ctail *)
-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
-#J #K #W #H #_ >H -H >ltail_length
-@(ex2_3_intro … J (K.ⓑ{I}V) W) /2 width=1 by length_pair/
-qed-.
-