proposition: Lemma fkind_pa x: formulap x -> ((P x = val_in \/ P x = val_eq ) <-> atomic_formulap x).
proof: Proof. move => fx. have Ha: atomic_formulap x -> P x = val_in \/ P x = val_eq. by move /atomic_formulaP => [_ _ _ _]. split => // hb; case: (equal_or_not (formula_len x) \0c) => lex0. by move/(flength0P fx): lex0. move: val_compare => [q0 q1 q2 q3 [q4 q5 q6 [q7 q8 q9]]]. move:(flength_nz fx lex0) => [hu hv hw]. move: hv => /next_formulasP; case. + done. + move => [_ h _]; case hb; rewrite h => h1; [ by case q5 | by case q2]. + move => [_ h _ _ _]; case hb; rewrite h => h1; [ by case q4 | by case q1]. + move => [_ h _ _ _]; case hb; rewrite h => h1; [ by case q6 | by case q3]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)