proposition: Theorem app_eq_unit (x y:list A) (a:A) : x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = [].
proof: Proof. destruct x; cbn. - intros ->. now left. - intros [= -> [-> ->] %app_eq_nil]. now right. Qed.
imports: PeanoNat