proposition: Lemma strip_in : forall (X: seq (T*T*T')) (a a':T) (b:T'), (a,a',b) \in X -> (a,b) \in (strip X).
proof: Proof. elim => [ | [[hd1 hd2] hdb] tl hi] //= a a' b. rewrite !in_cons. case/orP. - rewrite eqE /=. case/andP. case/andP => /= heq _ heq2. by rewrite (eqP heq) (eqP heq2) eq_refl. - move => h. by rewrite (hi a a' b h) orbT. Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)