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