Nuprl Rule : dependentIntersectionEqElimination

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:(a = b ∈ x:A ⋂ B), J ⊢ T ext !(!((!\\u.(!\\v.t)) Ax) Ax)

  BY dependentIntersectionEqElimination #$i u v ()

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

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

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