NF weak partition development: NominalAlphaRepairedBase001019Sik.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfSik (x y z u t : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_t : t ∉ A.fv) (dv_A_u : u ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_t_u : t ≠ u) (__dv_t_x : t ≠ x) (dv_t_y : t ≠ y) (dv_t_z : t ≠ z) (dv_u_x : u ≠ x) (dv_u_y : u ≠ y) (dv_u_z : u ≠ z) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsik A) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))) (Compiler.CompactSourceSyntax.synWex t (Compiler.CompactSourceSyntax.synWex u (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv t))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv t) (SemanticCore.Class.cv u)) A)))))))))

Checked nominal proof certificate identified upstream as nominal_df_sik.

Equations

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