Nominal proof certificates grouped in dependency order.

Certificates from ReplaySupport.CodeCover1.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnqinjcodecoverddndvStage1 (u : SemanticCore.Var) (P : SemanticCore.Class) (k : SemanticCore.Var) (Y : SemanticCore.Class) (dv_P_u : u ∉ P.fv) (hyp_cfbhnqinjcodecoverddndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem P Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbhnqinjcodecoverddndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem Y Compiler.CompactSourceSyntax.synCvv)) {Result : Type} (continuation : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss Y (Compiler.CompactSourceSyntax.synCun P Y)) → Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun P Y) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) → Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCres (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCres (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCres (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCres (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)))) → Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCres (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCres (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCres (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCres (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) → Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)) Y)) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwcn Y)))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnqinc Y (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synChnord Y)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso Y)) (Compiler.CompactSourceSyntax.synChnord Y))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqinc Y (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso Y))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqinc Y (Compiler.CompactSourceSyntax.synCun P Y)))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso P)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 P)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWss P (Compiler.CompactSourceSyntax.synCun P Y)) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y)))) → Result) : Result

Checked nominal proof certificate identified upstream as g_cfbhnqinjcodecoverddndv_stage1.

Equations

• One or more equations did not get rendered due to their size.

Certificates from ReplaySupport.CodeCover2.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnqinjcodecoverddndvStage2 (u : SemanticCore.Var) (P : SemanticCore.Class) (k : SemanticCore.Var) (Y : SemanticCore.Class) (dv_P_u : u ∉ P.fv) (hyp_cfbhnqinjcodecoverddndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem P Compiler.CompactSourceSyntax.synCvv)) (p0001 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun P Y) Compiler.CompactSourceSyntax.synCvv)) (p0010 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)))) (p0011 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) (p0023 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCvv)) (p0291 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) Compiler.CompactSourceSyntax.synCvv)) (p0292 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) Compiler.CompactSourceSyntax.synCvv)) (p0359 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso P)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 P)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))))) (p0360 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss P (Compiler.CompactSourceSyntax.synCun P Y))) (p0363 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))))) {Result : Type} (continuation : ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ⋯ ⋯) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))).imp (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))).imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))).imp (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))).imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))).imp ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))).imp ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))).imp ((Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCun P Y)).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCun P Y))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCun P Y))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synChwcodes (Compiler.CompactSourceSyntax.synCun P Y)))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcodes (Compiler.CompactSourceSyntax.synCun P Y))).imp ((Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcodes (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcodes (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y)))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y)))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv ⋯))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv ⋯) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv ⋯) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv ⋯)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCsn ⋯)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem ⋯ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem ⋯ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni ⋯) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ⋯ ⋯).imp (Compiler.CompactSourceSyntax.synWa ⋯ ⋯)) → Nominal.NPrf (⋯.imp ⋯) → Nominal.NPrf ⋯ → ⋯ → ⋯) : ⋯

Checked nominal proof certificate identified upstream as g_cfbhnqinjcodecoverddndv_stage2.

Certificates from ReplaySupport.CodeCover3.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnqinjcodecoverddndvStage3 (u : SemanticCore.Var) (P : SemanticCore.Class) (k : SemanticCore.Var) (Y : SemanticCore.Class) (p0001 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun P Y) Compiler.CompactSourceSyntax.synCvv)) (p0006 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (p0011 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) (p0023 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCvv)) (p0082 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synCvv)) (p0370 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))))) (p0395 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqinc P (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso P))) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))))) (p0419 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))) (p0421 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))))) (p0424 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))).imp (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))))) (p0425 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))).imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))))) (p0430 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))).imp (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))))) (p0431 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))).imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)))))))) (p0440 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)))) (p0444 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)))))) (p0458 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))))) (p0469 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))))) (p0481 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) (p0494 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))))) (p0555 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))))) (p0557 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y)))))) (p0565 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))))) (p0585 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))))) (p0590 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) (p0605 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))) (p0609 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))))) (p0626 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) Compiler.CompactSourceSyntax.synCvv)))) (p0628 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))))) (p0677 : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) Compiler.CompactSourceSyntax.synCvv))) (p0689 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1) ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))).imp ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) Compiler.CompactSourceSyntax.synCvv).imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))).imp ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))))))))) (p0690 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))))) {Result : Type} (continuation : ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → ⋯ → Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ ⋯ ∪ ⋯ ∪ ⋯) ⋯)) ⋯) ⋯)) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))).imp ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))) → Nominal.NPrf ((SemanticCore.Wff.all (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp ((Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) → Nominal.NPrf ((SemanticCore.Wff.all (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp ((Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))).imp (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))).biimp (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqinc P (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso P))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) Compiler.CompactSourceSyntax.synCvv)) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (SemanticCore.Class.cv u)))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) → Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCvv)) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) Compiler.CompactSourceSyntax.synCvv)) → Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv ⋯)) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 9) (SemanticCore.Wff.classEq (SemanticCore.Class.cv ⋯) (Compiler.CompactSourceSyntax.synCsn ⋯)))) → Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 9)) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf ((SemanticCore.Wff.classEq ⋯ ⋯).imp (SemanticCore.Wff.classEq ⋯ ⋯)) → Nominal.NPrf (⋯.imp ⋯) → Nominal.NPrf ⋯ → ⋯ → ⋯) : ⋯

Checked nominal proof certificate identified upstream as g_cfbhnqinjcodecoverddndv_stage3.