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

State before:
p : Nat → Formula
⊢ denote (universal p) = ∀ (x : Nat), denote (p x)
Tactic:
rfl
State after:
no goals