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; auto. intros l2 l3; case l3; simpl; (try (intros; discriminate)). intros b l H; exists (nil (A:=B)); exists l; exists b; (repeat (split; auto)). intros a0 l H l2 l3; case l3; simpl; (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; split; auto)). f_equal; auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat