proposition: Theorem same_length_ex : forall (a : A) l1 l2 l3, length (l1 ++ a :: l2) = length l3 -> exists l4, (exists l5, (exists b : B, length l1 = length l4 /\ length l2 = length l5 /\ l3 = l4 ++ b :: l5)).
proof: Proof. intros a l1; elim l1; simpl in |- *; auto. intros l2 l3; case l3; simpl in |- *; try (intros; discriminate). intros b l H; exists []; exists l; exists b; repeat (split; auto). intros a0 l H l2 l3; case l3; simpl in |- *; try (intros; discriminate). intros b l0 H0. case (H l2 l0); auto. intros l4 (l5, (b1, (HH1, (HH2, HH3)))). exists (b :: l4); exists l5; exists b1; repeat (simpl in |- *; split; auto). apply f_equal2 with (f := cons (A:=B)); auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)