proposition: Lemma formula_val_inc X a b (x := J val_in (J a b)) (V := formula_val X x): variablep a -> variablep b -> [/\ V = Val_of_inc X a b, sub V (formula_values X x) & forall f, inc f V <-> [/\ fgraph f, domain f = doubleton a b, inc (Vg f a) X, inc (Vg f b) X & inc (Vg f a) (Vg f b)]].
proof: Proof. move => va vb. move: val_compare => [q0 q1 q2 q3 [q4 q5 q6 [q7 q8 q9]]]. move: (fkind_in_p2 va vb) => [sa sb]. have vc: val_in = val_in \/ val_in = val_eq by left. have ->: V = Val_of_inc X a b. rewrite /V(formula_val_rec X sa) /formula_val_aux sb. by aw; Ytac0; Ytac0; Ytac0; Ytac0. rewrite /formula_values (free_vars_in va vb). split; [exact | apply: Zo_S |split ]. move => /Zo_P [/Zo_P [/setP_P pa [pb pc]] pd]; split => //. have adf: inc a (domain f) by rewrite - pc; fprops. move: (pa _ (fdomain_pr1 pb adf)) => /setX_P [_ _]; aw; trivial. have bdf: inc b (domain f) by rewrite - pc; fprops. by move: (pa _ (fdomain_pr1 pb bdf)) => /setX_P [_ _]; aw. move => [fgf df fa fb fc]; apply/Zo_P; split => //; apply/gfunctions_P2. split => // t /(range_gP fgf) [z zdf ->]. by move: zdf; rewrite df; case /set2_P => -> //; rewrite - sf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)