proposition: Lemma LS_nextP_pr2 X P n (Y:= (Vf (LS_rec X P) n)): sub P X -> natp n -> sub P Y /\ sub Y X.
proof: Proof. move => pa pb; rewrite /Y {Y}. move:(induction_defined_pr (LS_nextP X) P). rewrite -/(LS_rec _ _); move => [h1 h2 h3 h4]. move: n pb; apply:Nat_induction; first by rewrite h3; split. move => n nN [Hr1 Hr2]; rewrite (h4 _ nN). split; first by apply: (sub_trans Hr1); apply: (LS_nextP_pr1 Hr2). rewrite /LS_nextP => t/ funI_P [z za ->]. move/Zo_P: za => [ha [hb hc hd]]. have he: pformula_in X z. move /pformulas_inP: ha => [ka kb]; split => //; exact: (sub_trans kb Hr2). move: (pformula_inst_p1 hb hc) => [_ _ _ hf]. by move:(rep_i (hf _ hd)) => /Zo_S. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)