Nuprl Rule : dependentIntersectionElimination

This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
at https://github.com/vrahli/NuprlInCoq

H z:x:A ⋂ B, J ⊢ T ext !(!((!\\u.(!\\v.t)) Ax) Ax)

  BY dependentIntersectionElimination #$i u v ()

  H z:x:A ⋂ B, u:(z = z ∈ A), v:(z = z ∈ B[z/x]), J ⊢ T ext t

Definitions occuring in rule : axiom: Ax, dep-isect: x:A ⋂ B[x], equal: s = t ∈ T

Latex:
H z:x:A \mcap{} B, J \mvdash{} T ext !(!((!\mbackslash{}\mbackslash{}u.(!\mbackslash{}\mbackslash{}v.t)) Ax) Ax) BY dependentIntersectionElimination \#\$i u v () H z:x:A \mcap{} B, u:(z = z), v:(z = z), J \mvdash{} T ext t Date html generated: 2019_06_20-PM-04_11_56 Last ObjectModification: 2015_11_23-PM-03_41_58 Theory : rules Home Index