NF weak partition development: FocusedFVPaths.

theorem NFChoice.DefinitionLeaves.AlphaFocusedFV.fv_subset_cab_wrex_left {outer inner : SemanticCore.Var} {A : SemanticCore.Class} {p : SemanticCore.Wff} (houter : outer ∉ A.fv) (hinner : inner ∉ A.fv) : A.fv ⊆ (SemanticCore.Class.cab outer (Compiler.CompactSourceSyntax.synWrex inner A p)).fv

The class parameter remains free through cab outer (wrex inner A p).

theorem NFChoice.DefinitionLeaves.AlphaFocusedFV.fv_subset_ccompl_cab_wrex_left {outer inner : SemanticCore.Var} {A : SemanticCore.Class} {p : SemanticCore.Wff} (houter : outer ∉ A.fv) (hinner : inner ∉ A.fv) : A.fv ⊆ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab outer (Compiler.CompactSourceSyntax.synWrex inner A p))).fv

Complement preserves the preceding focused free-variable embedding.