proposition: Lemma project_comb : forall t l, In t l -> rwr (Pi pi V0 V1) t (Comb l).
proof: Proof. intros t l; induction l as [ | a l]. contradiction. simpl; set (sigma := (V0,a) :: (V1, Comb l) :: nil). assert (H1 : a = apply_subst sigma (Var V0)). simpl; rewrite eq_var_bool_refl; apply eq_refl. assert (H2 : Comb l = apply_subst sigma (Var V1)). simpl; rewrite eq_var_bool_refl; case_eq (eq_var_bool V1 V0). intro V1_eq_V0; apply False_rect; apply V0_diff_V1; apply sym_eq. generalize (eq_var_bool_ok V1 V0); rewrite V1_eq_V0; intro; assumption. intros _; apply eq_refl. assert (H3 : Term pi (a :: Comb l :: nil) = apply_subst sigma (Term pi (Var V0 :: Var V1 :: nil))). rewrite H1, H2; apply eq_refl. intros [t_eq_a | t_in_l]. subst t; do 2 left. rewrite H3, H1; apply instance; left. apply trans_clos_is_trans with (Comb l). apply IHl; assumption. rewrite H3, H2; do 2 left; apply instance; right. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)