proposition: Lemma fkind_ex_p1 x (a := (P (Q x))) (b := Q (Q x)): formulap x -> P x = val_ex -> [/\ x = J val_ex (J a b), variablep a, formulap b & formula_len b <c formula_len x].
proof: Proof. move => fp kx1. move: val_compare => [q0 q1 q2 q3 [q4 q5 q6 [q7 q8 q9]]]. case (equal_or_not (formula_len x) \0c) => ha. move /(flength0P fp): ha => /atomic_formulaP [_ _ _ _]. rewrite kx1; case => h; [by case: q6 | by case: q3]. case:(flength_nz fp ha); set F:= Vf _ _ => pa pb pc. case/next_formulasP: pb. + done. + by move => [_ h _ ];case:q9; rewrite - h. + by move => [_ h _ _ _];case:q8; rewrite - h. + move => [prx _ pqx ab bf]. rewrite - kx1 pqx prx. move:(NS_formula_len fp) => nN. move: (cpred_pr nN ha) => [sa ->]. have fa:= (formula_hi sa bf); split => //; apply/(cltSleP sa). exact:(proj33 (formula_len_pr fa) _ sa bf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)