proposition: Lemma disjP s1 s2 : disj_spec s1 s2 (disj s1 s2).
proof: Proof. rewrite /disj; case E: (all _ _). - by apply: disj_true; case: allP E. move: E; rewrite all_predC; move/negbFE. by case: hasPx=>// x H1 H2 _; apply: disj_false H1 H2. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq path) LemmaOverloading(ordtype prelude)