fact: Fixpoint is_subterm (s t : term) : bool := match t with | Var x => match s with Var y => eq_var_bool x y | _ => false end | Term f l => let fix is_subterm_list (l : list term) : bool := match l with | nil => false | t :: l => orb (is_subterm s t) (is_subterm_list l) end in orb (eq_bool t s) (is_subterm_list l) end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)