% $Id: forest.proof,v 1.1 1998/03/04 04:31:05 connolly Exp $
execute forest_Checks.lp
  declare variables foo: List[Int]
  prove ~(foo \in Domaux(empty)) by contradiction
      <> contradiction subgoal
      make passive forest.11
      normalize *Hyp with reversed forest.11
      [] contradiction subgoal
    [] conjecture
  declare variables li: List[Int], sl:Set[List[Int]]
  prove ~(sl = {}) => \E li (li \in sl)
    resume by induction on sl using SetBasics.1
      <> basis subgoal
      [] basis subgoal
      <> induction subgoal
      resume by specializing li to l
        <> specialization subgoal
        [] specialization subgoal
      [] induction subgoal
    [] conjecture
  prove Domaux(empty) = {} by contradiction
      <> contradiction subgoal
      display forestTheorem
      instantiate sl by Domaux(empty) in forestTheorem.3
      [] contradiction subgoal
    [] conjecture
  [] conjecture
qed
%% quit