proposition: Lemma FB_Pi : forall s t, one_step (Pi pi V0 V1) t s <-> In t (Pi_red s).
proof: Proof. intros s; pattern s; apply term_rec3; clear s. intros s t; simpl; split; intro H. inversion H; subst. inversion H0; subst. destruct t2 as [v2 | f2 l2]. inversion H3. discriminate. contradiction. intros f l IH t; split; intro H. inversion H; clear H; subst. inversion H0; clear H0; subst. destruct t2 as [v2 | f2 l2]; inversion H2; clear H2; subst f2; subst. simpl in H; injection H; clear H; intros H f2_eq_f; subst f. simpl Pi_red. simpl; generalize (F.Symb.eq_bool_ok pi pi); case (F.Symb.eq_bool pi pi); [intros _; left | intros pi_diff_pi; absurd (pi = pi)]; trivial. simpl in H; injection H; clear H; intros H f2_eq_f; subst f. simpl Pi_red. simpl; generalize (F.Symb.eq_bool_ok pi pi); case (F.Symb.eq_bool pi pi); [intros _; right; left | intros pi_diff_pi; absurd (pi = pi)]; trivial. assert (H' : In l1 (Pi_red_list l)). induction H2; simpl. apply in_or_app; left. rewrite in_map_iff. exists t1; split; trivial. rewrite <- IH; trivial; left; trivial. apply in_or_app; right. rewrite in_map_iff; exists l1; split; trivial. apply IHone_step_list; trivial. intros; apply IH; right; trivial. simpl; generalize (F.Symb.eq_bool_ok f pi); case (F.Symb.eq_bool f pi); [intros f_eq_pi | intros f_diff_pi]. subst f; destruct l as [ | t1 [ | t2 [ | t3 l]]]. contradiction. rewrite in_map_iff; exists l1; split; trivial. right; right; rewrite in_map_iff; exists l1; split; trivial. rewrite in_map_iff; exists l1; split; trivial. rewrite in_map_iff; exists l1; split; trivial. assert (H' : forall l', In l' ((fix Pi_red_list (l : list term) : list (list term) := match l with | nil => nil (A:=list term) | t :: lt => map (fun t' : term => t' :: lt) (Pi_red t) ++ map (fun l' : list term => t :: l') (Pi_red_list lt) end) l) -> one_step_list (one_step (Pi pi V0 V1)) l' l). intros l' H'. assert (H'' : In l' (Pi_red_list l)). clear IH H; induction l as [ | s l]; trivial. generalize l' H''; clear l' H H' H''; induction l as [ | s l]; intros l' H''. contradiction. simpl in H''; destruct (in_app_or _ _ _ H'') as [H1 | H2]. rewrite in_map_iff in H1; destruct H1 as [t' [H1' H1]]; subst l'. apply head_step. rewrite IH; trivial. left; trivial. rewrite in_map_iff in H2; destruct H2 as [l'' [H2' H2]]; subst l'. apply tail_step. apply IHl; trivial. intros; apply IH; right; trivial. revert H; simpl. generalize (F.Symb.eq_bool_ok f pi); case (F.Symb.eq_bool f pi); [intros f_eq_pi | intros f_diff_pi]. subst f; destruct l as [ | t1 [ | t2 [ | t3 l]]]. apply False_rect. intro H; rewrite in_map_iff in H; destruct H as [l' [H'' H]]; subst t. apply in_context; apply H'; trivial. intros [t_eq_t1 | [t_eq_t2 | H]]. assert (H1sigma : t1 = apply_subst ((V0,t1) :: (V1,t2) :: nil) (Var V0)). simpl; generalize (X.eq_bool_ok V0 V0); case (X.eq_bool V0 V0); [intros _ | intros V0_diff_V0; absurd (V0 = V0)]; trivial. assert (H2sigma : Term pi (t1 :: t2 :: nil) = apply_subst ((V0,t1) :: (V1,t2) :: nil) (Term pi (Var V0 :: Var V1 :: nil))). simpl; generalize (X.eq_bool_ok V0 V0); case (X.eq_bool V0 V0); [intros _ | intros V0_diff_V0; absurd (V0 = V0)]; trivial. generalize (X.eq_bool_ok V1 V0); case (X.eq_bool V1 V0); [intros V1_eq_V0; absurd (V0 = V1); trivial; subst V0 | intros _]; trivial. simpl; generalize (X.eq_bool_ok V1 V1); case (X.eq_bool V1 V1); [intros _ | intros V1_diff_V1; absurd (V1 = V1)]; trivial. subst t; pattern t1 at 1. rewrite H1sigma. pattern t1 at 1. rewrite H2sigma. apply at_top. apply instance. apply Pi1. assert (H1sigma : t2 = apply_subst ((V0,t1) :: (V1,t2) :: nil) (Var V1)). simpl; generalize (X.eq_bool_ok V1 V0); case (X.eq_bool V1 V0); [intros V1_eq_V0; absurd (V0 = V1); trivial; subst V0 | intros _]; trivial. simpl; generalize (X.eq_bool_ok V1 V1); case (X.eq_bool V1 V1); [intros _ | intros V1_diff_V1; absurd (V1 = V1)]; trivial. assert (H2sigma : Term pi (t1 :: t2 :: nil) = apply_subst ((V0,t1) :: (V1,t2) :: nil) (Term pi (Var V0 :: Var V1 :: nil))). simpl; generalize (X.eq_bool_ok V0 V0); case (X.eq_bool V0 V0); [intros _ | intros V0_diff_V0; absurd (V0 = V0)]; trivial. simpl; generalize (X.eq_bool_ok V1 V0); case (X.eq_bool V1 V0); [intros V1_eq_V0; absurd (V0 = V1); trivial; subst V0 | intros _]; trivial. simpl; generalize (X.eq_bool_ok V1 V1); case (X.eq_bool V1 V1); [intros _ | intros V1_diff_V1; absurd (V1 = V1)]; trivial. subst t; pattern t2 at 1. rewrite H1sigma. pattern t2 at 1. rewrite H2sigma. apply at_top. apply instance. apply Pi2. rewrite map_app in H; destruct (in_app_or _ _ _ H) as [H1 | H2]; clear H. rewrite in_map_iff in H1; destruct H1 as [l' [H'' H]]; subst t. apply in_context; apply H'; apply in_or_app; left; trivial. simpl in H2; rewrite <- app_nil_end in H2. rewrite in_map_iff in H2; destruct H2 as [l' [H'' H]]; subst t. apply in_context; apply H'; apply in_or_app; right. simpl; rewrite <- app_nil_end; trivial. intro H; rewrite in_map_iff in H; destruct H as [l' [H'' H]]; subst t. apply in_context; apply H'; trivial. intro H; rewrite in_map_iff in H; destruct H as [l' [H'' H]]; subst t. apply in_context; apply H'; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)