proposition: Lemma consec_ind k ks (P : A -> Prop) : uniq (k :: ks) -> P k -> (forall t1 t2, t2 \in ks -> consec (k::ks) t1 t2 -> P t1 -> P t2) -> forall t, t \in ks -> P t.
proof: Proof. move=>/= /andP [U1 U2] P0 IH t D; apply: consec_ind_raw IH _ _=>//. by rewrite inE D orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)