proposition: Lemma formula_val_or X a b (x := J val_or (J a b)) (V := formula_val X x) (Va := formula_val X a)(Vb := formula_val X b): formulap a -> formulap b -> [/\ V = Val_of_or X (free_vars a) (free_vars b) Va Vb, sub V (formula_values X x) & forall f, inc f V <-> (inc f (formula_values X x) /\ (inc (restr f (free_vars a)) Va \/ inc (restr f (free_vars b)) Vb))].
proof: Proof. move => pa pb;move: (fkind_or_p2 pa pb) => [sa sb]. move: val_compare => [q0 q1 q2 q3 [q4 q5 q6 [q7 q8 q9]]]. have ->: V = Val_of_or X (free_vars a) (free_vars b) Va Vb. rewrite /V (formula_val_rec X sa) /formula_val_aux. aw; Ytac0; Ytac0; Ytac0; Ytac0. have ha:= (NS_formula_len pa). have hb:= (NS_formula_len pb). move: (cmax_p1 (CS_nat ha)(CS_nat hb)) => [sd se]. have mN:natp (cmax (formula_len a)(formula_len b)) by apply:Gmax_E. by rewrite !LgV//; apply /Zo_P; split => //; rewrite sb; apply/cltSleP. have pc:= (free_vars_or pa pb). rewrite {3 4} /Val_of_or - pc -/x. split; [ exact | apply: Zo_S | ]. by split; [ move => /Zo_P | move => h; apply/Zo_P]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)