NF weak partition development: AlphaFocusedSupport.

Small proof combinators for expectation-guided alpha certificates. They keep generated wrappers from repeating dependent equality transport and Finset membership plumbing at every opaque formal subtree.

theorem NFChoice.DefinitionLeaves.AlphaFocusedSupport.reflOn_nil (support : Finset SemanticCore.Var) : AlphaTransport.ReflOn [] support

Every free variable has a reflexive alpha certificate in the empty binder environment.

theorem NFChoice.DefinitionLeaves.AlphaFocusedSupport.ReflOn.cons_of_not_mem {env : AlphaTransport.BinderEnv} {support : Finset SemanticCore.Var} {left right : SemanticCore.Var} (hleft : left ∉ support) (hright : right ∉ support) (tail : AlphaTransport.ReflOn env support) : AlphaTransport.ReflOn ((left, right) :: env) support

Add a genuinely renamed binder pair when neither endpoint occurs in the support.

theorem NFChoice.DefinitionLeaves.AlphaFocusedSupport.freshVar_not_mem_of_subset {small large : Finset SemanticCore.Var} (offset : ℕ) (hsub : small ⊆ large) : ReplaySupport.freshVar large offset ∉ small

Freshness descends along an explicitly supplied support inclusion.

theorem NFChoice.DefinitionLeaves.AlphaFocusedSupport.subset_erase_of_subset_of_not_mem {small large : Finset SemanticCore.Var} {binder : SemanticCore.Var} (hsub : small ⊆ large) (hnot : binder ∉ small) : small ⊆ large.erase binder

Insert a known subset beneath an erasure whose binder is absent from it.