Theorem: Cpdt.Chapter3.Formula.swapper_universal (Cpdt/Chapter3/Reflexive.lean)

State before:
p : Nat → Formula
⊢ swapper (universal p) = universal fun x => swapper (p x)
Tactic:
rfl
State after:
no goals