NF weak partition development: NominalAlphaRepairedBase001015Ins2k.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfIns2k (x y z v u t : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_t : t ∉ A.fv) (dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ 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_v : t ≠ v) (_dv_t_x : t ≠ x) (dv_t_y : t ≠ y) (dv_t_z : t ≠ z) (dv_u_v : u ≠ v) (_dv_u_x : u ≠ x) (dv_u_y : u ≠ y) (dv_u_z : u ≠ z) (_dv_v_x : v ≠ x) (dv_v_y : v ≠ y) (dv_v_z : v ≠ z) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCins2k 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.synWex v (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv t)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv u) (SemanticCore.Class.cv v))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv t) (SemanticCore.Class.cv v)) A))))))))))

Checked nominal proof certificate identified upstream as nominal_df_ins2k.

Equations

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