oracle 対応範囲拡大

[hinarid]

現行の wani では，Pi 型の後件に app 型が来る際に対応しておらず，以下のような問題が解けない
Pi 型の後件に App 型が来た際やそれ以外に対応が必要となるような扱いを検討する．

test =
  let
    sigEnv = [
                ("alien",U.Pi (U.Entity) (U.Pi U.Entity U.Type)),
                ("cola",U.Pi (U.Entity) (U.Pi U.Entity U.Type)),
                ("juice",U.Pi (U.Entity) (U.Pi U.Entity U.Type)),
                ("nomu",U.Pi U.Entity (U.Pi (U.Entity) (U.Pi U.Entity U.Type)))
              ]
    varEnv = [(U.Sigma (U.Entity) (U.Sigma (U.Entity) (U.App (U.App (U.Con "alien") (U.Var 0)) (U.Var 1)))), U.Pi (U.Sigma (U.Entity) (U.Sigma (U.Entity) (U.App (U.App (U.Con "alien") (U.Var 0)) (U.Var 1)))) (U.Sigma (U.Sigma (U.Entity) (U.Sigma (U.Entity) (U.App (U.App (U.Con "cola") (U.Var 0)) (U.Var 1)))) (U.Sigma (U.Entity) (U.App (U.App (U.App (U.Con "nomu") (U.Var 0)) (U.Proj U.Fst (U.Var 2))) (U.Proj U.Fst (U.Var 1)))))]
    pre_type = U.App (U.App (U.Con "juice") (U.Proj U.Fst (U.Proj U.Snd (U.Var 0)))) (U.Proj U.Fst (U.Proj U.Snd (U.Proj U.Fst (U.App (U.Var 1) (U.Var 0)))))
  in (True,PB.executeWithDepth 5 (U.ProofSearchQuery sigEnv varEnv pre_type))