proposition: Lemma formula_val_i X x: formulap x -> sub (formula_val X x) (formula_values X x).
proof: Proof. move => fx. case: (equal_or_not (formula_len x) \0c) => ha. move/(flength0P fx):ha => /atomic_formulaP [pa qa qb qc pc]. case: pc => h. by move:(proj32 (formula_val_inc X qb qc)); rewrite qa - h pa. by move:(proj32 (formula_val_eq X qb qc)); rewrite qa - h pa. move:(flength_nz fx ha) => [mN hc hd]. move/next_formulasP:hc; case. + done. + move => [pc pv qx]; move: (proj32 (formula_val_not X (formula_hi mN qx))). by rewrite - pv pc. + move => [pc pv qa qb qc]. move: (proj32 (formula_val_or X (formula_hi mN qb)(formula_hi mN qc))). by rewrite - pv qa pc. + move => [pa pb pc pd pe]. move: (proj32(formula_val_ex X pd (formula_hi mN pe))). by rewrite pc - pb pa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)