[STATEMENT]
lemma pA2: "Fr_2 \<F> \<Longrightarrow> \<forall>A. A \<^bold>\<approx> \<C> A \<^bold>\<leftharpoonup> \<B>(\<^bold>\<midarrow>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A w. A w = (\<C> A \<^bold>\<leftharpoonup> \<B> (\<^bold>\<midarrow>A)) w
[PROOF STEP]
using pB1 dual_def fp3
[PROOF STATE]
proof (prove)
using this:
\<forall>A w. \<B> A w = (A \<^bold>\<leftharpoonup> \<I> A) w
?\<phi>\<^sup>d \<equiv> \<lambda>X. ?\<phi>\<^sup>c (\<^bold>\<midarrow>X)
Fr_2 \<F> \<Longrightarrow> \<C>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B>\<^sup>d

goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A w. A w = (\<C> A \<^bold>\<leftharpoonup> \<B> (\<^bold>\<midarrow>A)) w
[PROOF STEP]
unfolding equal_op_def conn
[PROOF STATE]
proof (prove)
using this:
\<forall>A w. \<B> A w = (A w \<and> \<not> \<I> A w)
?\<phi>\<^sup>d \<equiv> \<lambda>X w. \<not> ?\<phi> (\<lambda>w. \<not> X w) w
Fr_2 \<F> \<Longrightarrow> \<forall>X w. (\<C> X w = X w) = \<B>\<^sup>d X w

goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A w. A w = (\<C> A w \<and> \<not> \<B> (\<lambda>w. \<not> A w) w)
[PROOF STEP]
by smt