proposition: Lemma formula_val_not X a (x := J val_not a) (V := formula_val X x) (Va := formula_val X a): formulap a -> [/\ V = Val_of_not X (free_vars a) Va, sub V (formula_values X x) & forall f, inc f V <-> inc f (formula_values X x) /\ ~ inc f Va].
proof: Proof. move => pa;move: (fkind_not_p2 pa) => [sa sb]. move: val_compare => [q0 q1 q2 q3 [q4 q5 q6 [q7 q8 q9]]]. have fv: (free_vars (J val_not a)) = free_vars a by apply: free_vars_not. have ->: V = Val_of_not X (free_vars a) Va. rewrite /V (formula_val_rec X sa) /formula_val_aux; aw. Ytac0; Ytac0; Ytac0; Ytac0. rewrite fv LgV//; apply/Zo_P; split => //; rewrite sb. apply: (cltS (NS_formula_len pa)). rewrite - fv;split; [ exact | by move => t /setC_P [] | ]. by split; [ move /setC_P | move => h; apply /setC_P]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)