proposition: Lemma tset_nextP E x: inc x (tset_next E) <-> [\/ exists2 y, inc y E & x = Tp y, exists y z, [/\ inc y E, inc z E & x = Tx y z] | inc x E].
proof: Proof. split. case/setU2_P; last by move => xe; constructor 3. case /setU2_P; first by move/funI_P => h; constructor 1. move /funI_P => [y /setX_P [ya yb yc] ->]; constructor 2. by exists (P y), (Q y); rewrite /Tx ya. case => h. - by apply /setU2_P;left; apply /setU2_P;left; apply/funI_P. - apply /setU2_P;left; apply /setU2_P;right; apply/funI_P. by move: h => [y [z [yE zE ->]]]; exists (J y z) => //; apply: setXp_i. - by apply /setU2_P;right. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)