proposition: Lemma induction_defined_pr_set0 E h a (f := induction_defined_set0 h a E): inc a E -> (forall n x, inc x E -> natp n -> inc (h n x) E) -> [/\ function_prop f Nat E, Vf f \0c = a & forall n, natp n -> Vf f (csucc n) = h n (Vf f n)].
proof: Proof. move=> aE ag. have st := (integer_induction_stable0 aE ag). have [sf [ff _] f0 fs] := (induction_defined_pr0 h a). move: (change_target_pr ff st); rewrite -/(induction_defined_set0 h a E) -/f. rewrite sf; move => [pa pd]. split => //; first by rewrite -f0 pd //; exact: NS0. by move => n nb; rewrite (pd _ (NS_succ nb)) (fs _ nb) -pd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)