fact: Fixpoint fv_com (c: com) : IdentSet.t := match c with | SKIP => IdentSet.empty | ASSIGN x a => fv_aexp a | SEQ c1 c2 => IdentSet.union (fv_com c1) (fv_com c2) | IFTHENELSE b c1 c2 => IdentSet.union (fv_bexp b) (IdentSet.union (fv_com c1) (fv_com c2)) | WHILE b c => IdentSet.union (fv_bexp b) (fv_com c) end.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)