proposition: Lemma LS_nextP_pr1 X P: sub P X -> sub P (LS_nextP X P).
proof: Proof. rename P into Pa. move=> spx a ap; move: (spx a ap) => ax. move: (proj1 (formula_ext3 ax)) (proj2 (formula_ext3 ap)). set z := J _ _ => ha hb. by apply/funI_P; exists z; [apply: (hb _ ax) | rewrite ha rep_set1 ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)