fact: Fixpoint included_list (l1 l2:list A) {struct l1} : bool := match l1 with | nil => true | x::l1 => andb (mem_bool x l2) (included_list l1 l2) end.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)