fact: Fixpoint map_PExpr (e : PExpr S) : PExpr C := match e with | PEc c => PEc (C_of_S c) | PEX p => PEX p | PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2) | PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2) | PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2) | PEopp e => PEopp (map_PExpr e) | PEpow e n => PEpow (map_PExpr e) n end.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl