proposition: Lemma app_comm_cons' {A : Set}: forall (a : A) As As', As ++ (a :: As') = (As ++ (a :: nil)) ++ As'.
proof: Proof. intros; rewrite <- app_assoc; reflexivity. Defined.
imports: Coq.Arith.Arith Coq.Lists.List Coq.Sets.Ensembles Coq.Strings.String Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.Common.DecideableEnsembles