proposition: Lemma symb_in_term_unfold : forall f t, symb_in_term f t = match t with | Var _ => false | Term g l => orb (eq_symb_bool f g) (symb_in_term_list f l) end.
proof: Proof. intros g t; case t; intros; reflexivity. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)