Nuprl Rule : freeFromAtomApplication

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  ⊢ a#f x:B[x/v]

  BY freeFromAtomApplication v:A ⟶ B

  H  ⊢ a#f:v:A ⟶ B
  H  ⊢ a#x:A

Definitions occuring in rule : apply: f a, function: x:A ⟶ B[x], free-from-atom: a#x:T, axiom: Ax

Latex:
H \mvdash{} a\#f x:B[x/v] BY freeFromAtomApplication v:A {}\mrightarrow{} B H \mvdash{} a\#f:v:A {}\mrightarrow{} B H \mvdash{} a\#x:A Date html generated: 2019_06_20-PM-04_11_58 Last ObjectModification: 2015_11_25-PM-03_57_48 Theory : rules Home Index