Theorem: LeanSAT.Model.PropFun.hasUniqueExtension_refl (LeanSAT/Model/PropVars.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ : PropFun ν
⊢ hasUniqueExtension X X φ
Tactic:
simp [hasUniqueExtension]
State after:
no goals