NF weak partition development: NominalWPPReplayChunk015Compact001Part010.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnqordantisym (C R : SemanticCore.Class) (dv_C_R : Disjoint C.fv R.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCref C) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCtrans C)) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCconnex C)) (Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp C C)))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synClnqord R C) Compiler.CompactSourceSyntax.synCantisym (Compiler.CompactSourceSyntax.synClnquo R C)))

Checked nominal proof certificate identified upstream as g_lnqordantisym.

Equations

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