proposition: Theorem simplify : forall t t' p rm, interp_pos_atom p rm -> interp_tree t rm -> tree_beq (simplify' t p) t' = true -> interp_tree t' rm.
proof: Proof. intros t t' p rm Hp Ht Hs. rewrite <- (internal_tree_dec_bl _ _ Hs). generalize (proj1 (simplify'_correct t p rm Hp)). intuition. Qed.
imports: Reals List Bool Gappa_common