fact: Fixpoint AssignableEverything (sr_list : list StoreRefList) : bool := match sr_list with | nil => match NotSpecifiedAssignableClause with | \everything => true | _ => false end | sr::sr_list' => match sr with | \everything => true | _ => AssignableEverything sr_list' end end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)