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