proposition: Theorem transform_atom_bound_correct : forall f, stable_expr f -> stable_atom (transform_atom_bound (transform_expr f)).
proof: Proof. now intros f Hf [[l|] e [u|]|x y l u|x y|x y|fmt x|fmt x] ; simpl ; split ; repeat rewrite (transform_expr_correct _ Hf). Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library