proposition: Theorem transform_once_correct : forall uv tr t, convert_tree uv t -> convert_tree uv (transform_once tr t).
proof: Proof. intros uv [f Hf|f Hf|f Hf|f Hf|f Hf] t Ht ; simpl. now apply transform_tree_atom_correct. now apply transform_tree_atom'_correct. apply transform_tree_atom_correct with (2 := Ht). now apply transform_atom_bound_correct. apply transform_tree_atom_correct with (2 := Ht). now apply transform_atom_expr_correct. now apply Hf. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library