proposition: Lemma flength0P x: formulap x -> (formula_len x = \0c <-> atomic_formulap x).
proof: Proof. have qc:= formulas_rec0. move => /formula_len_pr [pa pb pc]; rewrite /atomic_formulap - qc. split => h; [ue | exact(cle0 (pc _ NS0 h)) ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)