(datatype proplog

  if (not (element? P [& =>]))
  P : symbol;
  ____________
  P : atom;

  P : atom;
  ________________
  P : conjunction;

  P : conjunction; Q : conjunction;
  ========================
  [P & Q] : conjunction;

  P : conjunction; Q : atom;
  ==========================
  [P => Q] : hypothesis; 

   P : atom;
   ________________
   P : hypothesis;)

(define backchain  
  {(list hypothesis) --> conjunction --> boolean} 
   Context Succeedent -> (backchain* Succeedent Context Context))

(define backchain*
   {conjunction --> (list hypothesis) --> (list hypothesis) --> boolean}
   P [Q | _] _ -> true  	where (== P Q) \\ hyp
   [P & Q] _ Context
   -> (and (backchain* P Context Context)
           (backchain* Q Context Context))  \\ &-right
   Q [[P => Q] | Hypotheses] Context  
   -> (or (backchain* P Context Context) \\ &-left
            (backchain* Q Hypotheses Context)) \\ choice point!
   Q [_ | Hypotheses] Context -> (backchain* Q Hypotheses Context)         
   _ _ _ -> false)