proposition: Lemma rev_cons_invert : forall A (x1 x2 : A) ls1 ls2, ls1 ++ [x1] = ls2 ++ [x2] -> x1 = x2 /\ ls1 = ls2.
proof: Proof. intros; apply (f_equal _ _ (@rev _)) in H. repeat rewrite rev_app_distr in H; simpl in H. inversion H; intuition auto using rev_involutive. apply (f_equal _ _ (@rev _)) in H2. repeat rewrite rev_involutive in *; auto. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)