proposition: Lemma finite_set_induction2 (A B:property): (forall a, A (singleton a) -> B (singleton a)) -> (forall a b, (nonempty a -> A a -> B a) -> nonempty a -> A(a +s1 b) -> B(a +s1 b)) -> forall x, finite_set x -> nonempty x -> A x -> B x.
proof: Proof. move=> fA fr; apply: finite_set_induction; first by move=> [t /in_set0]. move=> a b sa. case: (emptyset_dichot a) => pa. have ->: (a +s1 b = singleton b) by rewrite pa; exact: set0_U2. by move => _; apply: fA. by move => _; apply:fr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)