fact: Fixpoint transform_tree_atom (t : RTree) : RTree := match t with | rtTrue => rtTrue | rtFalse => rtFalse | rtAtom a => rtAtom (chg_atom a) | rtNot t => rtNot (transform_tree_atom t) | rtAnd t1 t2 => rtAnd (transform_tree_atom t1) (transform_tree_atom t2) | rtOr t1 t2 => rtOr (transform_tree_atom t1) (transform_tree_atom t2) | rtImpl t1 t2 => rtImpl (transform_tree_atom t1) (transform_tree_atom t2) end.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library