Nominal proof certificates grouped in dependency order.

Certificates from ReplaySupport.WellOrderPullback1.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPwpullwesetimpndvStage1 (x y f r : SemanticCore.Var) {Result : Type} (continuation : Nominal.NPrf Compiler.CompactSourceSyntax.synWtru → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCref (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1) (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv y)))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv f)) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv f))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv f))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))))) → Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv f) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4))) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)))) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (SemanticCore.Class.cv x))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)))) → Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCvv)) → Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv)) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCref (SemanticCore.Class.cv x))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))).imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)))))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5) Compiler.CompactSourceSyntax.synWtru)) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))).imp (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))).imp (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x)))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))) → Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv ⋯) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv ⋯) (SemanticCore.Class.cv x)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem ⋯ (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Wff.classMem ⋯ (SemanticCore.Class.cv x)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (⋯.imp ⋯)) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ⋯) → Nominal.NPrf ⋯ → ⋯ → ⋯) : Result

Checked nominal proof certificate identified upstream as g_pwpullwesetimpndv_stage1.

Equations

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

Certificates from ReplaySupport.WellOrderPullback2.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPwpullwesetimpndvStage2 (x y f r : SemanticCore.Var) (p0000 : Nominal.NPrf Compiler.CompactSourceSyntax.synWtru) (p0004 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y)))) (p0018 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))) (p0022 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))) (p0027 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv y))))) (p0036 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv f)))) (p0039 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv f)))) (p0045 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))))) (p0047 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) Compiler.CompactSourceSyntax.synCvv)) (p0050 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)))) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))))))) (p0055 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))))))) (p0059 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))))))) (p0066 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) (p0082 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))))) (p0090 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))))) (p0102 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x))))) (p0115 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCvv))) (p0117 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv))) (p0130 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))).imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))))))) (p0132 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5) Compiler.CompactSourceSyntax.synWtru))) (p0134 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))).imp (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))))) (p0135 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))).imp (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))))) (p0137 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)))) (p0140 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x)))) (p0141 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))))) (p0162 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))))))) (p0165 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))))))) (p0169 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))))) (p0172 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)))))) (p0185 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))))) (p0190 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))))) (p0193 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))))) (p0195 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))) (p0201 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))))) (p0202 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))))) (p0212 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))))) (p0278 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))))))) (p0282 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))).imp ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))))))) (p0283 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))))) (p0289 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCtrans (SemanticCore.Class.cv y))))) (p0290 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCtrans (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv)))) (p0293 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (SemanticCore.Class.cv r)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 6)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 6))))))) (p0294 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (SemanticCore.Class.cv r)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 6)))))) {Result : Type} (continuation : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (SemanticCore.Class.cv y)))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCtrans (SemanticCore.Class.cv x))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 6)) (SemanticCore.Class.cv r)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 6)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 6)) (SemanticCore.Class.cv r)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 6)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))))).imp ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))))).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))))))) → Result) : Result

Checked nominal proof certificate identified upstream as g_pwpullwesetimpndv_stage2.

Certificates from ReplaySupport.WellOrderPullback3.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPwpullwesetimpndvStage3 (x y f r : SemanticCore.Var) (p0000 : Nominal.NPrf Compiler.CompactSourceSyntax.synWtru) (p0004 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y)))) (p0022 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))) (p0027 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv y))))) (p0042 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv f)))) (p0046 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv f) Compiler.CompactSourceSyntax.synCvv)) (p0101 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (SemanticCore.Class.cv x)))) (p0113 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCvv)) (p0115 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCvv))) (p0116 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv)) (p0117 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv))) (p0126 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCref (SemanticCore.Class.cv x)))) (p0277 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))))))) (p0318 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (SemanticCore.Class.cv y))))) (p0331 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)))))) (p0335 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))))))) (p0437 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))))) (p0452 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCtrans (SemanticCore.Class.cv x)))) (p0517 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))))) (p0537 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 6)) (SemanticCore.Class.cv r)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 6)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)))))) (p0538 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 6)) (SemanticCore.Class.cv r)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 6)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)))))) (p0556 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))))))) (p0561 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))))))) (p0574 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))))))) (p0581 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))))).imp ((Compiler.CompactSourceSyntax.synW3a Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))))).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)))))))) {Result : Type} (continuation : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCantisym (SemanticCore.Class.cv x))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCconnex (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCstrict (SemanticCore.Class.cv x))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) Compiler.CompactSourceSyntax.synC0)) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) Compiler.CompactSourceSyntax.synC0))).imp ((Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) Compiler.CompactSourceSyntax.synC0).imp (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv x)))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) Compiler.CompactSourceSyntax.synC0))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) Compiler.CompactSourceSyntax.synC0))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) Compiler.CompactSourceSyntax.synCvv)) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) Compiler.CompactSourceSyntax.synC0))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp ((Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) Compiler.CompactSourceSyntax.synC0).imp (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) (SemanticCore.Class.cv y)))) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) (SemanticCore.Class.cv y))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) Compiler.CompactSourceSyntax.synC0))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y)))) → Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCwe Compiler.CompactSourceSyntax.synCwe) → Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCstrict (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCfound (SemanticCore.Class.cv y)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCfound (SemanticCore.Class.cv y)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) Compiler.CompactSourceSyntax.synCvv))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCfound (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv r)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2))) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))).imp (SemanticCore.Wff.objEq (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))))) (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2))) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))).imp (SemanticCore.Wff.objEq (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))))))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2))) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))).imp (SemanticCore.Wff.objEq (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))))) (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))).imp (SemanticCore.Wff.objEq (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))))))) → Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCfound (Compiler.CompactSourceSyntax.synCopab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2) (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2))) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))).imp (SemanticCore.Wff.objEq (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))))))) → Result) : Result

Checked nominal proof certificate identified upstream as g_pwpullwesetimpndv_stage3.