Proofgold Proof

The subproof is completed by applying pack_b_0_eq2 with {x3 ∈ setexp (ap x0 0) (ap x0 0)|Field_automorphism_fixing x0 x1 x3}, lam_comp (ap x0 0), λ x3 x4 . x2 x4 x3.