-let subst = subst 0 false;;\r
-\r
-let subst_in_problem (sub: var * t) (p: problem) =\r
-print_endline ("-- SUBST " ^ string_of_t (V (fst sub)) ^ " |-> " ^ string_of_t (snd sub));\r
- {p with\r
- div=subst sub p.div;\r
- conv=subst sub p.conv;\r
- stepped=(fst sub)::p.stepped;\r
- sigma=sub::p.sigma}\r
+let subst top = subst top 0 false;;\r
+let mk_app = mk_app true;;\r
+\r
+let eta_eq =\r
+ let rec aux t1 t2 = match t1, t2 with\r
+ | L t1, L t2 -> aux t1 t2\r
+ | L t1, t2 -> aux t1 (A(`Some (ref true),lift 1 t2,V 0))\r
+ | t1, L t2 -> aux (A(`Some (ref true),lift 1 t1,V 0)) t2\r
+ | V a, V b -> a = b\r
+ | A(_,t1,t2), A(_,u1,u2) -> aux t1 u1 && aux t2 u2\r
+ | _, _ -> false\r
+ in aux ;;\r
+\r
+(* is arg1 eta-subterm of arg2 ? *)\r
+let eta_subterm u =\r
+ let rec aux lev t = eta_eq u (lift lev t) || match t with\r
+ | L t -> aux (lev+1) t\r
+ | A(_, t1, t2) -> aux lev t1 || aux lev t2\r
+ | _ -> false\r
+ in aux 0\r
+;;\r
+\r
+let subst_in_problem ?(top=true) ((v, t) as sub) p =\r
+print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t);\r
+ let sigma = sub::p.sigma in\r
+ let sub = (`Inherit, v, t) in\r
+ let div = try subst top sub p.div with B -> raise (Done sigma) in\r
+ let conv = try subst false sub p.conv with B -> raise (Fail(-1,"p.conv diverged")) in\r
+ {p with div; conv; sigma}\r