proposition: Lemma formula_not_simp X a: formulap a -> formula_val X (J val_not (J val_not a)) = formula_val X a.
proof: Proof. move => pa. move: (proj33 (formula_val_not X pa)). set x := (J val_not a); set E := (formula_val X x) => H. have pb: formulap (J val_not a) by exact (proj1 (fkind_not_p2 pa)). move: (proj33 (formula_val_not X pb)). set y := (J val_not x); set F := (formula_val X y). have e1: (formula_values X y) = (formula_values X x). by rewrite /formula_values (free_vars_not pb). have e2: (formula_values X x) = (formula_values X a). by rewrite /formula_values (free_vars_not pa). rewrite e1 -/E => Hf. set_extens t. by move /Hf => [ta tb]; ex_middle ba; case tb; apply /H. move => h; apply/Hf; move: (formula_val_i pa h); rewrite e2 => qb. by split => // /H [hu hv]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)