Nominal proof certificates grouped in dependency order.

Certificates from ReplaySupport.CodeCover4.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnqinjcodecoverddndvStage4 (u : SemanticCore.Var) (P : SemanticCore.Class) (k : SemanticCore.Var) (Y : SemanticCore.Class) (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)))))) (p0374 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))))) (p0400 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))) (p0403 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (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))))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))).imp (Compiler.CompactSourceSyntax.synWb (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 u))) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)) (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.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))))) (p0406 : 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.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)) (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.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))) (p0415 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (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.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))).imp (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2) (Compiler.CompactSourceSyntax.synWa (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.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) 2))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))))))) (p0417 : 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.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)))) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2) (Compiler.CompactSourceSyntax.synWa (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.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) 2))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))))))) (p0420 : 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)))))) (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)))))))) (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)))))) (p0451 : 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))))) (p0453 : 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)))))) (p0455 : 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)))))) (p0462 : 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))))) (p0466 : 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)))))) (p0478 : 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))))))) (p0480 : 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))))))) (p0489 : 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))))))) (p0503 : 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)))))) (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))))))) (p0570 : 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)))))))) (p0580 : 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)))))) (p0586 : 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) 7))) (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) 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))))))) (p0621 : 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.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.synCvv))) (p0624 : Nominal.NPrf ((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 (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) Compiler.CompactSourceSyntax.synCvv))) (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)))) (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))) (p0679 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (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) 6))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))) (p0697 : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) Compiler.CompactSourceSyntax.synCvv))) (p0705 : 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 ((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)))))))) (p0722 : 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 ((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)))).imp (SemanticCore.Wff.classEq (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))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))))))) (p0724 : Nominal.NPrf ((SemanticCore.Wff.classEq (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))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (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.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))) (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) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))))) (p0726 : 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.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))) (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) 7))) (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.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.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))))) (p0747 : 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) 7))) (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)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))))))) (p0752 : 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} ∪ 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))))))) (p0754 : 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))))))) (p0766 : 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)) ⋯ ⋯))).imp ⋯)) (p0771 : ⋯) (p0773 : ⋯) (p0779 : ⋯) (p0781 : ⋯) (p0825 : ⋯) (p0827 : ⋯) (p0828 : ⋯) (p0834 : ⋯) (p0846 : ⋯) (p0938 : ⋯) (p0939 : ⋯) (p0955 : ⋯) (p0961 : ⋯) {Result : ⋯} (continuation : ⋯) : ⋯

Checked nominal proof certificate identified upstream as g_cfbhnqinjcodecoverddndv_stage4.

Certificates from ReplaySupport.CodeCover5.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnqinjcodecoverddndvStage5 (u : SemanticCore.Var) (P : SemanticCore.Class) (k : SemanticCore.Var) (Y : SemanticCore.Class) (p0000 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss Y (Compiler.CompactSourceSyntax.synCun P Y))) (p0001 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun P Y) Compiler.CompactSourceSyntax.synCvv)) (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)))))) (p0013 : 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)))))) (p0022 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCvv)) (p0036 : 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)))))) (p0050 : 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)))))))) (p0069 : 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))))) (p0082 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synCvv)) (p0084 : 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)) (p0140 : 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))))) (p0282 : 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))))))) (p0286 : 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))))))) (p0288 : 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))))))) (p0296 : 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)))))) (p0306 : 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))))) (p0310 : 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))) (p0330 : 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))))))) (p0364 : 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))))) (p0534 : 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)))))) (p0541 : 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))))) (p0548 : 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))))))))) (p0553 : 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))))) (p0791 : 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)))))))) (p0794 : 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)))))))) (p0796 : 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)))))) (p0798 : 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)))))) (p0805 : 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))))) (p0807 : 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)))))))) (p0809 : 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))))))) (p0815 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (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)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y))) (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.synChnord (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))) (p0820 : 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))))))) (p0825 : 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))) (p0827 : 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))))) (p0831 : 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))))))) (p0839 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) Compiler.CompactSourceSyntax.synCvv)) (p0848 : 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))) (p0973 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp ((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.synCec (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))))) (p0974 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (SemanticCore.Class.cv u)).imp (Compiler.CompactSourceSyntax.synWb (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)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))) (p0977 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (SemanticCore.Class.cv u)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (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.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))) (p0986 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) Compiler.CompactSourceSyntax.synCvv))) (p0997 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (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))))))) (p1023 : 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.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))))))) (p1089 : 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.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))))))) (p1345 : 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.all (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2) (SemanticCore.Wff.all (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1) (SemanticCore.Wff.all (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.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.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)))))))))) {Result : Type} (continuation : 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.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synChwcn (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.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (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.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 (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 (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))))) → Nominal.NPrf ((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)))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCvv)) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (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)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u))))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synChnqmap1 (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.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCpw1 (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 (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (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.synCrn (SemanticCore.Class.cv k)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))) (SemanticCore.Wff.all (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2) (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2 Compiler.CompactSourceSyntax.synCsset) (Compiler.CompactSourceSyntax.synCins3 (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))))) Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2 Compiler.CompactSourceSyntax.synCsset) (Compiler.CompactSourceSyntax.synCins3 (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))))))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2 Compiler.CompactSourceSyntax.synCsset) (Compiler.CompactSourceSyntax.synCins3 (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))))) (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) (Compiler.CompactSourceSyntax.synCins2 Compiler.CompactSourceSyntax.synCsset)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) (Compiler.CompactSourceSyntax.synCins3 (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))))).neg) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) (Compiler.CompactSourceSyntax.synCins2 Compiler.CompactSourceSyntax.synCsset)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))) Compiler.CompactSourceSyntax.synCsset)) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))).biimp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) → 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.synCrn (SemanticCore.Class.cv k)) Compiler.CompactSourceSyntax.synCvv)) → Result) : Result

Checked nominal proof certificate identified upstream as g_cfbhnqinjcodecoverddndv_stage5.

Equations

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

Certificates from ReplaySupport.CodeCover6.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnqinjcodecoverddndvStage6 (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)) (p0286 : 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))))))) (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))))) (p0442 : 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))))) (p0558 : 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)))))) (p0560 : 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))))))) (p0562 : 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))))))) (p0839 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) Compiler.CompactSourceSyntax.synCvv)) (p0842 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) Compiler.CompactSourceSyntax.synCvv)) (p0853 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) Compiler.CompactSourceSyntax.synCvv)) (p0859 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 9) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 9)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))))))) (p0860 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 9)) Compiler.CompactSourceSyntax.synCvv)) (p0871 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 9)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 9)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))))) (p0880 : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) Compiler.CompactSourceSyntax.synCvv))) (p0888 : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) Compiler.CompactSourceSyntax.synCvv))) (p0902 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) Compiler.CompactSourceSyntax.synCvv)) (p0903 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 10)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 10)) Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))))) (p0906 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) Compiler.CompactSourceSyntax.synCvv)) (p0907 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) (p0939 : Nominal.NPrf Compiler.CompactSourceSyntax.synWtru) (p0957 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) Compiler.CompactSourceSyntax.synCvv))) (p1123 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))))))) (p1618 : 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.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))))) (p1621 : 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.synCun P Y)))))) (p1643 : Nominal.NPrf ((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)))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCvv))) (p1645 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (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)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)))))) (p1646 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))) (p1652 : 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 (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (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.synCrn (SemanticCore.Class.cv k)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))))) (p1653 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) (p1654 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))) (SemanticCore.Wff.all (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2) (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))))))) (p1655 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2 Compiler.CompactSourceSyntax.synCsset) (Compiler.CompactSourceSyntax.synCins3 (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))))) Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2 Compiler.CompactSourceSyntax.synCsset) (Compiler.CompactSourceSyntax.synCins3 (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))))))))) (p1656 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2 Compiler.CompactSourceSyntax.synCsset) (Compiler.CompactSourceSyntax.synCins3 (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))))) (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) (Compiler.CompactSourceSyntax.synCins2 Compiler.CompactSourceSyntax.synCsset)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) (Compiler.CompactSourceSyntax.synCins3 (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))))).neg)) (p1658 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))))) (Compiler.CompactSourceSyntax.synCins2 Compiler.CompactSourceSyntax.synCsset)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))) Compiler.CompactSourceSyntax.synCsset))) (p1659 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))) Compiler.CompactSourceSyntax.synCsset))) (p1662 : 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.synCrn (SemanticCore.Class.cv k)) Compiler.CompactSourceSyntax.synCvv))) {Result : Type} (continuation : 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.synCrn (SemanticCore.Class.cv k))) 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 (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 (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u))).imp (Compiler.CompactSourceSyntax.synWb (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)))) (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.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))) → Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (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 (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))) → 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.synWbr (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synChnqmap1 (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 (Compiler.CompactSourceSyntax.synCun P Y)))))) → Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u))) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChnqmap1 (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 (Compiler.CompactSourceSyntax.synCun P Y)))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synChnqmap1 (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 (Compiler.CompactSourceSyntax.synCun P Y)))))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)) (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 (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)) (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 (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k)))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k)))) (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.synCrn (SemanticCore.Class.cv k)))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k)))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k)))) (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.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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k)))) (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.synCrn (SemanticCore.Class.cv k)))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k)))) (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.synCrn (SemanticCore.Class.cv k)))) (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.synCrn (SemanticCore.Class.cv k)))) (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.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp ((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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k)))) (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.synCrn (SemanticCore.Class.cv k)))) (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.synCrn (SemanticCore.Class.cv k))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))))) → 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.synCdm (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (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.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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k))))) (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.synCrn (SemanticCore.Class.cv k)))) (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.synCrn (SemanticCore.Class.cv k)))) (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.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))))) → 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.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwcn (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.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))).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 ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).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.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (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.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))))))) → 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.synCrn (SemanticCore.Class.cv k)))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) Compiler.CompactSourceSyntax.synCvv)) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)))).imp (Compiler.CompactSourceSyntax.synWb (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)))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (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.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))))))) → Result) : Result

Checked nominal proof certificate identified upstream as g_cfbhnqinjcodecoverddndv_stage6.