filter_challenge

Filter.v

(*   SCase := "test x = false" : String.string *)
(*   Case := "iom_seq" : String.string *)
(*   X : Type *)
(*   test : X -> bool *)
(*   x : X *)
(*   xs : list X *)
(*   ys : list X *)
(*   zs : list X *)
(*   Hiom : in_order_merge xs ys zs *)
(*   Hl1 : filter test (x :: xs) = x :: xs *)
(*   Hl2 : filter test ys = [] *)
(*   IHHiom : filter test xs = xs -> filter test ys = [] -> filter test zs = xs *)
(*   Htest_x : test x = false *)
(*   H0 : filter test xs = x :: xs *)
(*   ============================ *)
(*    filter test zs = x :: xs *)

(* subgoal 2 (ID 1987) is: *)
(*  filter test (y :: x :: zs) = x :: xs *)