proposition: Lemma in_prec: forall h l l', In l h -> prec (h++[l']) l l'.
proof: Proof. intros. apply in_split in H. destruct H as [h1 [h2 H]]. unfold prec. exists h1. exists h2. exists nil. rewrite H. 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)