fact: Fixpoint app_assoc {A : Set} (As As' As'' : list A): As ++ (As' ++ As'') = (As ++ As') ++ As'' := match As as As return As ++ (As' ++ As'') = (As ++ As') ++ As'' with | nil => eq_refl _ | a :: As => (f_equal (fun l => a :: l) (app_assoc As As' As'')) end.
imports: Coq.Arith.Arith Coq.Lists.List Coq.Sets.Ensembles Coq.Strings.String Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.Common.DecideableEnsembles