fact: Fixpoint norm_ep (e:ExprP) : ExprP := match e with | EPeq e1 e2 => EPeq (norm_ez e1) (norm_ez e2) | EPlt e1 e2 => EPlt (norm_ez e1) (norm_ez e2) | EPle e1 e2 => EPle (norm_ez e1) (norm_ez e2) | EPgt e1 e2 => EPgt (norm_ez e1) (norm_ez e2) | EPge e1 e2 => EPge (norm_ez e1) (norm_ez e2) | EPimpl e1 e2 => EPimpl (norm_ep e1) (norm_ep e2) | EPequiv e1 e2 => EPequiv (norm_ep e1) (norm_ep e2) | EPand e1 e2 => EPand (norm_ep e1) (norm_ep e2) | EPor e1 e2 => EPor (norm_ep e1) (norm_ep e2) | EPneg e => EPneg (norm_ep e) | EPraw p => EPraw p end.
imports: BinInt