proposition: Lemma consec_indX (ks : seq A) (P : A -> Prop) : uniq ks -> (forall t1, t1 \in ks -> ks = t1 :: behead ks -> P t1) -> (forall t1 t2, t1 \in ks -> t2 \in ks -> consec ks t1 t2 -> P t1 -> P t2) -> forall t, t \in ks -> P t.
proof: Proof. case: ks=>//= k ks /andP [K U] H1 H2; apply: consec_ind_raw=>//. - by apply: (H1 k)=>//; rewrite inE eq_refl. move=>t1 t2 N Cx; apply: H2=>//. - by rewrite (consec_mem Cx). by rewrite inE N orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)