fact: Fixpoint EvalParams (formals : list Param) (actuals : list Expression) (st : State.t) {struct actuals} : list (Value) := match formals , actuals with | f::fs, e::es => (EvalParam f e st) :: EvalParams fs es st | _ , _ => nil end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)