"cwff ((Op,ρ),Φ) (cBOX m fl) ⟷
  (m ∈ Op ∧ ρ m = length fl ∧
   (∀f. f ∈ list.set fl ⟶ cwff ((Op,ρ),Φ) f))"

"cwff (τ,Φ) (cBOX m fl) ⟷
  (m ∈ (fst τ) ∧ (snd τ) m = length fl ∧
   (∀f. f ∈ list.set fl ⟶ cwff (τ,Φ) f))"

Sledgehammering...
cvc4 found a proof...
verit found a proof...
cvc4 found a proof...
cvc4 found a proof...
vampire found a proof...
vampire found a proof...
cvc4: Try this: by (smt (verit) prod.collapse) (> 1.0 s, timed out)
cvc4: Duplicate proof
cvc4: Duplicate proof
vampire: Try this: by (metis surjective_pairing) (> 1.0 s, timed out)

Isar proof (8.2 s):
proof -
  obtain cc :: "('a, 'b) cform list ⇒ 'b set ⇒ ('a ⇒ nat) ⇒ 'a set ⇒ ('a, 'b) cform" where
    "∀X1 X2 X3 X4. (∃X5. ¬ cwff ((X4, X3), X2) X5 ∧ X5 ∈ list.set X1) ⟶ ¬ cwff ((X4, X3), X2) (cc X1 X2 X3 X4) ∧ cc X1 X2 X3 X4 ∈ list.set X1"
    by moura
  then obtain cca :: "('a, 'b) cform list ⇒ 'b set ⇒ ('a ⇒ nat) ⇒ 'a set ⇒ ('a, 'b) cform" where
    "∀a cs B f A. (cwff ((A, f), B) (cBOX a cs) ∨ a ∉ A ∨ ¬ cwff ((A, f), B) (cca cs B f A) ∧ cca cs B f A ∈ list.set cs ∨ length cs ≠ f a) ∧ (a ∈ A ∧ (∀c. cwff ((A, f), B) c ∨ c ∉ list.set cs) ∧ length cs = f a ∨ ¬ cwff ((A, f), B) (cBOX a cs))"
    by (metis (full_types) cwff_cBOX0)
  then show ?thesis
    by (smt (z3) surjective_pairing)
qed
verit: Try this: by (smt (verit) prod.exhaust_sel) (> 1.0 s, timed out)
vampire: Try this: by (metis cBOX_def prod.exhaust_sel) (> 1.0 s, timed out)

Isar proof (6.4 s):
proof -
  obtain cc :: "('a ⇒ nat) ⇒ 'a set ⇒ 'b set ⇒ ('a, 'b) cform list ⇒ ('a, 'b) cform" where
    "∀X0 X2 X3 X4. (∃X5. X5 ∈ list.set X4 ∧ ¬ cwff ((X2, X0), X3) X5) ⟶ cc X0 X2 X3 X4 ∈ list.set X4 ∧ ¬ cwff ((X2, X0), X3) (cc X0 X2 X3 X4)"
    by moura
  then obtain cca :: "('a ⇒ nat) ⇒ 'a set ⇒ 'b set ⇒ ('a, 'b) cform list ⇒ ('a, 'b) cform" where
    "∀f a A B cs. (cwff ((A, f), B) (cBOX a cs) ∨ a ∉ A ∨ length cs ≠ f a ∨ cca f A B cs ∈ list.set cs ∧ ¬ cwff ((A, f), B) (cca f A B cs)) ∧ (a ∈ A ∧ length cs = f a ∧ (∀c. c ∉ list.set cs ∨ cwff ((A, f), B) c) ∨ ¬ cwff ((A, f), B) (cBOX a cs))"
    by (metis (full_types) cwff_cBOX0)
  then show ?thesis
    by (smt (z3) prod.exhaust_sel)
qed
Done

lemma
  assumes
    "⋀Op ρ Φ m fl. cwff ((Op,ρ),Φ) (cBOX m fl) ⟷
       (m ∈ Op ∧ ρ m = length fl ∧
       (∀f. f ∈ list.set fl ⟶ cwff ((Op,ρ),Φ) f))"
  shows
    "cwff (τ,Φ) (cBOX m fl) ⟷
    (m ∈ (fst τ) ∧ (snd τ) m = length fl ∧
     (∀f. f ∈ list.set fl ⟶ cwff (τ,Φ) f))"
  using assms
  by (metis prod.collapse)

find_theorems name:Pair
thm Pair(2)

found 14 theorem(s):
  Product_Type.case_prod_Pair: (λ(x, y). (x, y)) = id
  Product_Type.scomp_Pair: scomp ?x Pair = ?x
  Product_Type.Pair_scomp: scomp (Pair ?x) ?f = ?f ?x
  Product_Type.Pair_def:
    (?a, ?b) = Abs_prod (Pair_Rep ?a ?b)
  Basic_BNF_LFPs.Pair_def_alt:
    Pair ≡
    λa b. Basic_BNF_LFPs.xtor
           (BNF_Composition.id_bnf (a, b))
  BNF_Fixpoint_Base.Pair_transfer:
    rel_fun ?A (rel_fun ?B (rel_prod ?A ?B)) Pair Pair
  BNF_Fixpoint_Base.case_prod_Pair_iden:
    (case ?p of (x, y) ⇒ (x, y)) = ?p
  Product_Type.Pair_Rep_def:
    Pair_Rep ?a ?b = (λx y. x = ?a ∧ y = ?b)
  Product_Type.Pair_vimage_Sigma:
    Pair ?x -` Sigma ?A ?f =
    (if ?x ∈ ?A then ?f ?x else {})
  Filter.filtermap_Pair:
    filtermap (λx. (?f x, ?g x)) ?F
    ≤ filtermap ?f ?F ×⇩F filtermap ?g ?F
  BNF_Greatest_Fixpoint.subst_Pair:
    ?P ?x ?y ⟹ ?a = (?x, ?y) ⟹ ?P (fst ?a) (snd ?a)
  BNF_Least_Fixpoint.ssubst_Pair_rhs:
    (?r, ?s) ∈ ?R ⟹ ?s' = ?s ⟹ (?r, ?s') ∈ ?R
  Product_Type.Pair_inject:
    (?a, ?b) = (?a', ?b') ⟹
    (?a = ?a' ⟹ ?b = ?b' ⟹ ?R) ⟹ ?R
  Filter.filterlim_Pair:
    filterlim ?f ?G ?F ⟹
    filterlim ?g ?H ?F ⟹
    LIM x ?F. (?f x, ?g x) :> ?G ×⇩F ?H

case (Pair a b)

1. (a, b) = (a, b) ⟹
    cwff ((a, b), Φ) (cBOX m fl) =
    (m ∈ fst (a, b) ∧
     snd (a, b) m = length fl ∧
     (∀f. f ∈ list.set fl ⟶ cwff ((a, b), Φ) f))

  cwff ((?Op, ?ρ), ?Φ) (cBOX ?m ?fl) =
    (?m ∈ ?Op ∧
     ?ρ ?m = length ?fl ∧
     (∀f. f ∈ list.set ?fl ⟶ cwff ((?Op, ?ρ), ?Φ) f))

then show ?thesis using cwff_cBOX0 apply (unfold Pair(2))