proposition: Theorem transform_tree_atom_correct : stable_atom chg_atom -> stable_tree transform_tree_atom.
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. now apply Hs. now apply Hs. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library