proposition: Lemma prec_trans: forall p h s l l' l'', step_star (init p) h s -> prec h l l' -> prec h l' l'' -> prec h l l''.
proof: Proof. unfold prec; firstorder subst. eapply step_star_NoDup in H. destruct H; simpl in H. assert (x ++ l' :: (x0 ++ l'' :: x1) = (x2 ++ l :: x3) ++ l' :: x4). rewrite <- app_assoc. rewrite <- H0. reflexivity. clear H0. eapply NoDup_map_middle in H2. 2: eauto. 2: auto. destruct H2. rewrite H0. exists x2. exists (x3 ++ l' :: x0). exists x1. simpl. rewrite <- app_assoc. rewrite <- app_assoc. rewrite app_assoc. rewrite <- app_assoc. reflexivity. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)