proposition: Theorem prepare_goal : forall uv t, convert_tree uv (rtNot (transform trans (normalize_tree t false))) -> convert_tree uv t.
proof: Proof. intros uv t. change (not (convert_tree uv (transform trans (normalize_tree t false))) -> convert_tree uv t). intros H. destruct (decidable_tree uv t) as [H'|H']. easy. contradict H. apply transform_correct. now apply normalize_tree_correct. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library