proposition: Lemma card_LS_nextP X P : cardinal (LS_nextP X P) <=c cardinal P +c aleph0.
proof: Proof. have pa: cardinal (LS_nextP X P) <=c cardinal (LS_nextP_aux X P). apply: fun_image_smaller. have: sub (LS_nextP_aux X P) (pformulas_in P) by apply: Zo_S. by move/sub_smaller; rewrite cardinal_pformulas_in; apply: cleT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)