proposition: Lemma induction_defined_pr_set1 E h a p (f := induction_defined_set1 h a p E): natp p -> inc a E -> (forall n x, inc x E -> n <c p -> inc (h n x) E) -> [/\ function_prop f Nat E, Vf f \0c = a, (forall n, n <c p -> Vf f (csucc n) = h n (Vf f n)) & (forall n, natp n -> ~ (n <=c p) -> Vf f n = a)].
proof: Proof. move=> pN aE ag. have st := (integer_induction_stable1 pN aE ag). have [sf [ff _] f0 fs1 fs2] := (induction_defined_pr1 h a pN). move: (change_target_pr ff st); rewrite -/(induction_defined_set1 h a E) -/f. rewrite sf; move => [pa pd]. split => //; first by rewrite -f0 pd //; exact: NS0. move => n np. have nN:= NS_lt_nat np pN. by rewrite (pd _ nN) (pd _ (NS_succ nN)) fs1. by move => n nN np; rewrite (pd _ nN) (fs2 _ nN np). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)