proposition: Lemma prec_pre_prec: forall h l l' l'', (prec (h ++ [l]) l' l'' /\ l <> l'') -> prec h l' l''.
proof: Proof. unfold prec; firstorder. apply prec_split in H; firstorder. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)