fact: Fixpoint convert_tree (t : RTree) : Prop := match t with | rtTrue => True | rtFalse => False | rtAtom a => convert_atom a | rtNot t => not (convert_tree t) | rtAnd t1 t2 => (convert_tree t1) /\ (convert_tree t2) | rtOr t1 t2 => (convert_tree t1) \/ (convert_tree t2) | rtImpl t1 t2 => (convert_tree t1) -> (convert_tree t2) end.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library