proposition: Lemma projection_one_step_list : forall f l1 l2, refl_trans_clos (one_step_list (one_step R)) l2 l1 -> refl_trans_clos (one_step R) (projection (Term f l2)) (projection (Term f l1)).
proof: Proof. intros h l3 l4 H; simpl. generalize (nth_error_ok_in (P h) l4). case_eq (nth_error l4 (P h)). intros s4 H4 K; destruct (K _ (eq_refl _)) as [l41 [l42 [L4 H4']]]; clear K H4. generalize (nth_error_ok_in (P h) l3). case_eq (nth_error l3 (P h)). intros s3 H3 K; destruct (K _ (eq_refl _)) as [l31 [l32 [L3 H3']]]; clear K H3. rewrite <- L4 in L3. subst l3 l4. apply (refl_trans_clos_one_step_list_refl_trans_clos_one_step _ _ _ _ _ _ (sym_eq L3) H). intros H3 _. absurd (length l41 < length l41). apply Nat.lt_irrefl. assert (L : length l4 = length l3). inversion H. trivial. apply rwr_list_length_eq with (one_step R); assumption. assert (L' := nth_error_none _ _ H3). rewrite <- L4 in L'; rewrite <- L in L'; subst l4. apply Nat.lt_le_trans with (length (l41 ++ s4 :: l42)); trivial. rewrite length_app; rewrite Nat.add_comm; simpl. apply le_n_S; apply NatCompat.le_add_l. intros H4 _. generalize (nth_error_ok_in (P h) l3). case_eq (nth_error l3 (P h)). intros s3 H3 K; destruct (K _ (eq_refl _)) as [l31 [l32 [L3 H3']]]; clear K H3. absurd (length l31 < length l31). apply Nat.lt_irrefl. assert (L : length l4 = length l3). inversion H. trivial. apply rwr_list_length_eq with (one_step R); assumption. assert (L' := nth_error_none _ _ H4). rewrite <- L3 in L'; rewrite L in L'; subst l3. apply Nat.lt_le_trans with (length (l31 ++ s3 :: l32)); trivial. rewrite length_app; rewrite Nat.add_comm; simpl. apply le_n_S; apply NatCompat.le_add_l. intros H3 _. inversion H. left. right. apply general_context; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)