NF weak partition development: NAR4C087C001Part004.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfFdrowfib (A B C R : SemanticCore.Class) (d : SemanticCore.Var) (__dv_A_B : Disjoint A.fv B.fv) (__dv_A_C : Disjoint A.fv C.fv) (__dv_A_R : Disjoint A.fv R.fv) (dv_A_d : d ∉ A.fv) (__dv_B_C : Disjoint B.fv C.fv) (__dv_B_R : Disjoint B.fv R.fv) (dv_B_d : d ∉ B.fv) (__dv_C_R : Disjoint C.fv R.fv) (dv_C_d : d ∉ C.fv) (dv_R_d : d ∉ R.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdrowfib R A B C) (SemanticCore.Class.cab d (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv d)) C) (Compiler.CompactSourceSyntax.synCfdrowrel R A B))))

Checked nominal proof certificate identified upstream as nominal_df_fdrowfib.

Equations

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