proposition: Theorem transform_tree_atom'_correct : stable_atom_tree chg_atom -> forall t, convert_tree t -> convert_tree (transform_tree_atom' t).
proof: Proof. intros Hs t. induction t as [| |a|t Ht|t1 Ht1 t2 Ht2|t1 Ht1 t2 Ht2|t1 Ht1 t2 Ht2] ; simpl ; intuition. destruct t ; intuition. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library