proposition: Lemma LS_res_p0 X P x: inc x (LS_res X P) <-> (exists2 n, inc n Nat & inc x (Vf (LS_rec X P) n)).
proof: Proof. move:(induction_defined_pr (LS_nextP X) P). rewrite -/LS_res; move => [h1 [ff h2] h3 h4]. split. move/setU_P => [z za zb]; move: (h2 _ zb); rewrite h1. by move => [t ta tb]; exists t => //; rewrite /LS_rec - tb. move => [n nN xv]; apply/setU_P; exists (Vf (LS_rec X P) n) => //. by rewrite - h1 in nN; apply: Vf_target. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)