proposition: Lemma formula_ex_simp X a b: variablep a -> formulap b -> ~(inc a (free_vars b)) -> formula_val X (J val_ex (J a b)) = formula_val X b.
proof: Proof. move => pa pb pc. move: (proj33 (formula_val_ex X pa pb)). set x := (J val_ex (J a b)); set E := (formula_val X x). have e1: free_vars x = free_vars b. by rewrite (free_vars_ex pa pb) setC1_eq. have ->: (formula_values X x) = (formula_values X b). by rewrite /formula_values e1. have aux: forall f, inc f (formula_values X b) -> f = restr f (free_vars x). move => f /gfunctions_P2 [pha hb hc]. apply: fgraph_exten; [ exact | fprops | by aw; rewrite e1 |]. by move => t tdf /=; rewrite LgV// //e1 - hb. move => H; set_extens t. by move /H=> [ha [g gr]]; rewrite - (aux _ (formula_val_i pb gr)) => ->. move => tb; move:(formula_val_i pb tb) => h1; apply/H; split => //; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)