proposition: Lemma elt_eq_unit l1 l2 (a b : A) : l1 ++ a :: l2 = [b] -> a = b /\ l1 = [] /\ l2 = [].
proof: Proof. intros Heq. apply app_eq_unit in Heq. now destruct Heq as [[Heq1 Heq2]|[Heq1 Heq2]]; inversion_clear Heq2. Qed.
imports: PeanoNat