proposition: Theorem transform_expr_correct : stable_expr chg_expr -> stable_expr transform_expr.
proof: Proof. unfold stable_expr. intros Hf t. induction t ; simpl ; rewrite Hf ; simpl ; try easy. now rewrite IHt. now rewrite IHt1, IHt2. now rewrite IHt. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library