(define backchain  
   Context Succeedent  -> (backchain* Succeedent Context Context))

(define backchain*
   P [P | _] _ -> true  \\ hyp
   [P & Q] _ Context
   -> (and (backchain* P Context Context)
           (backchain* Q Context Context))  
   Q [[P => Q] | Hypotheses] Context  
   -> (or (backchain* P Context Context) 
          (backchain* Q Hypotheses Context)) \\ choice point!
   Q [_ | Hypotheses] Context -> (backchain* Q Hypotheses Context)      
   _ _ _ -> false)

(backchain q [[p => q] [r => q] r])