proposition: Lemma integer_induction_stable1 E h a p: natp p -> inc a E -> (forall n x, inc x E -> n <c p -> inc (h n x) E) -> sub (target (induction_defined1 h a p)) E.
proof: Proof. move=> pN aE ahE t tt. have [sf sjf f0 fs lf] := (induction_defined_pr1 h a pN). have [x xsf ->] :=(proj2 sjf _ tt). move: x xsf; rewrite sf;apply: Nat_induction; first by ue. move=> n nN vE. case:(p_or_not_p (n <c p)) => np. by rewrite (fs _ np); apply: ahE. rewrite lf; fprops; move /cleSltP; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)