proposition: Lemma app_inj_pivot x1 x2 y1 y2 (a : A): x1 ++ a :: x2 = y1 ++ a :: y2 -> ((In a x1 /\ In a y2) \/ (In a x2 /\ In a y1)) \/ (x1 = y1 /\ x2 = y2).
proof: Proof. induction y1 as [|b y1 IHy] in x1 |- *; intros [[-> H]|[x' [-> H]]]%app_eq_cons. - right. now injection H. - subst y2. left; left. split; [apply in_eq | apply in_elt]. - injection H as -> ->. left; right. split; [ apply in_elt | apply in_eq ]. - symmetry in H. apply IHy in H as [[[]|[]]|[]]. + left; left. split; [apply in_cons|]; assumption. + left; right. split; [|apply in_cons]; assumption. + right. split; congruence. Qed.
imports: PeanoNat