proposition: Lemma prec_in: forall (h: list Label)(l l': Label), prec h l l' -> (In l h /\ In l' h).
proof: Proof. intros. unfold prec in H. destruct H as [h1 H]. destruct H as [h2 H]. destruct H as [h3 H]. rewrite H. split. simpl. apply in_or_app. right. apply in_eq. apply in_or_app. right. apply in_or_app. right. apply in_eq. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)