proposition: Lemma var_case2 : forall n v f l, rpo n (Var v) (Term f l) -> var_in_term_list v l = true .
proof: Proof. intros m v f l v_lt_t; inversion v_lt_t as [ f2 l2 u s s_in_l v_le_s | | | ]; subst. generalize s s_in_l v_le_s; clear v_lt_t s s_in_l v_le_s; pattern l; apply (list_rec3 size); clear l. intro n; induction n as [ | n]; intros [ | t l] Sl s s_in_l v_le_s. contradiction. simpl in Sl; absurd (1 <= 0); auto with arith. refine (Nat.le_trans _ _ _ _ Sl); apply Nat.le_trans with (size t). apply size_ge_one. apply Nat.le_add_r. contradiction. simpl in s_in_l; destruct s_in_l as [s_eq_t | s_in_l]. rewrite (@equiv_rpo_equiv_3 _ _ _ s_eq_t) in v_le_s. inversion v_le_s; subst. inversion H; subst; rewrite var_in_term_list_equation; simpl; rewrite eq_var_bool_refl; trivial. inversion H as [g k u1 s' s'_in_k v_le_s' | | |]; subst; rewrite var_in_term_list_equation; simpl. assert (Sk : list_size size k <= n). apply le_S_n; refine (Nat.le_trans _ _ _ _ Sl); simpl; apply le_n_S; rewrite (list_size_fold size k); auto with arith. rewrite (IHn k Sk s' s'_in_k v_le_s'); simpl; trivial. assert (Sl' : list_size size l <= n). apply le_S_n; refine (Nat.le_trans _ _ _ _ Sl); simpl; apply (Nat.add_le_mono_r 1 (size t) (list_size size l)); apply size_ge_one. rewrite var_in_term_list_equation; rewrite (IHn l Sl' s s_in_l v_le_s); destruct t as [v' | g k]. case (X.eq_bool v v'); trivial. case (var_in_term_list v k); 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)