proposition: Theorem transform_correct : forall l uv t, convert_tree uv t -> convert_tree uv (transform l t).
proof: Proof. intros l uv t Ht. rewrite <- (rev_involutive l). induction (rev l) as [|h l' Hl] ; simpl. easy. unfold transform. rewrite fold_left_app. simpl. apply transform_once_correct. apply Hl. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library