proposition: Lemma pformula_ex a b X (x := formula_ex2) (g := variantL \1c \2c a b) (y := J x g): transitive_set X -> inc a X -> inc b X -> [/\ pformula y, pclosed y, pformula_in X y & (pformula_vals X y) = \1c <-> (sub a b)].
proof: Proof. move => h ax bx. move: (formula_ex2_pr h) => [pa pb pc pd]. have va: P y = x by rewrite /y; aw. have vb: Q y = g by rewrite /y; aw. have vfg: fgraph g by rewrite /g; fprops. have dg: domain g = free_vars x by rewrite variant_d. have pe: pformula y. rewrite /pformula va vb dg /g /y;split => //;fprops. have pf:pclosed y. by rewrite /pclosed /pfree_vars va vb dg setC_v. have g1: (Vg g \1c) = a by rewrite /g variant_V_a. have g2: (Vg g \2c) = b by rewrite /g variant_V_b //; fprops. have pg: sub (range g) X. move => t; move/(range_gP vfg). move => [u udf ->]; move: udf; rewrite dg pc; case/set2_P => ->; ue. have ph: inc g (formula_values X formula_ex2) by apply/gfunctions_P2; split. split => //; first by split => //; rewrite vb. move: (pfree_vars_closed_pr X pf); rewrite va vb - g1 - g2 => H. split; first by move /H /pd => [_ ]. move => h1; apply/H; apply/pd; split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)