proposition: Lemma formula_val_ex X a b (x := J val_ex (J a b)) (V := formula_val X x) (Vb := formula_val X b): variablep a -> formulap b -> [/\ V = Val_of_ex X (free_vars x) Vb, sub V (formula_values X x) & forall f, inc f V <-> (inc f (formula_values X x) /\ exists2 g, inc g Vb & f = restr g (free_vars x))].
proof: Proof. move => pa pb;move: (fkind_ex_p2 pa pb)=> [sa sb]. have pc:=free_vars_ex pa pb. move: val_compare => [q0 q1 q2 q3 [q4 q5 q6 [q7 q8 q9]]]. have hN := NS_formula_len pb. have ->: V = Val_of_ex X (free_vars x) Vb. rewrite /V (formula_val_rec X sa) /formula_val_aux; aw. Ytac0; Ytac0; Ytac0; Ytac0; rewrite LgV//. apply/Zo_P; split => //; rewrite sb; apply: (cltS hN). split; [done | apply:Zo_S |by split; [ move => /Zo_P | move => h; apply/Zo_P]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)