proposition: Lemma term_rec3_mem : forall P : term -> Type, (forall v : variable, P (Var v)) -> (forall (f : symbol) (l : list term), (forall t : term, mem equiv t l -> P t) -> P (Term f l)) -> forall t : term, P t.
proof: Proof. intros P Hvar Hterm. apply term_rec2; induction n; intros t Size_t. absurd (1 <= 0); auto with arith; apply Nat.le_trans with (size t); trivial; apply size_ge_one. destruct t as [ x | f l ]; trivial; apply Hterm; intros; apply IHn; apply Nat.lt_succ_r. apply Nat.lt_le_trans with (size (Term f l)); trivial. destruct (mem_split_set _ _ equiv_bool_ok _ _ H) as [t' [l1 [l2 [t_eq_t' [H' _]]]]]. simpl in t_eq_t'; simpl in H'; subst l. rewrite (equiv_same_size t_eq_t'). apply size_direct_subterm; simpl; apply in_or_app; right; left; trivial. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)