Theorem: Smt.Reconstruct.Quant.miniscopeN (Smt/Reconstruct/Quant/Lemmas.lean)

State before:
α : Type u
ps : List (α → Prop)
⊢ (∀ (x : α), andN (List.map (fun x_1 => x_1 x) [])) = andN (List.map (fun x => ∀ (x_1 : α), x x_1) [])
Tactic:
simp [andN]
State after:
no goals