proposition: Lemma free_vars_or a b (x := J val_or (J a b)): formulap a -> formulap b -> free_vars x = free_vars a \cup free_vars b.
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 hc:~(val_or = val_in \/ val_or = val_eq) by case => h; fprops. rewrite (free_vars_rec sa) /free_vars_aux; aw; 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. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)