fact: Fixpoint ConcatinateStoreRefs (sr_list : list StoreRefList) : list StoreRef := match sr_list with | nil => nil | \nothing :: sr_list' => ConcatinateStoreRefs sr_list' | \everything :: sr_list' => nil | StoreRefs srl :: sr_list' => srl +++ ConcatinateStoreRefs sr_list' end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)