proposition: Lemma formula_or_simp X a: formulap a -> formula_val X (J val_or (J a a)) = formula_val X a.
proof: Proof. move => pa. move: (proj33 (formula_val_or X pa pa)). set Va := (formula_val X a). set V := (formula_val X (J val_or (J a a))). rewrite /formula_values (free_vars_or pa pa) setU2_id => H. have ha: forall f, inc f (gfunctions (free_vars a) X) -> (restr f (free_vars a)) = f. move => f /gfunctions_P2 [qa qb qc]. apply: fgraph_exten; [ fprops | exact | by aw | aw => t tv; rewrite LgV// ]. set_extens f. by move /H => [qa]; rewrite (ha _ qa); case. move => qa; move: (formula_val_i pa qa) => qb. by apply/H; split => //; left; rewrite (ha _ qb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)