proposition: Lemma substrate_special_equivalence a b x: inc a x -> inc b x -> substrate(special_equivalence a b x) = x.
proof: Proof. move=> ax bx; rewrite/ special_equivalence. apply: substrate_union_diag. by move=> t /set2_P => [][] ->; apply/setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)