proposition: Lemma rept_union_pr x (f := rept_union x): f \0c = x /\ (forall n, natp n -> f (csucc n) = union (f n)).
proof: Proof. move: (induction_defined_pr union x) => [pa pb pc pd]; split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)