proposition: Lemma app_inj_tail : forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b.
proof: Proof. intros x y a b [l [[-> Hl %eq_sym]|[-> Hl %eq_sym]]] %app_eq_app; apply elt_eq_unit in Hl as [? [-> ?]]; now rewrite app_nil_r. Qed.
imports: PeanoNat