### Nuprl Lemma : tree_node-right_wf

`∀[E:Type]. ∀[v:tree(E)].  tree_node-right(v) ∈ tree(E) supposing ↑tree_node?(v)`

Proof

Definitions occuring in Statement :  tree_node-right: `tree_node-right(v)` tree_node?: `tree_node?(v)` tree: `tree(E)` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` ext-eq: `A ≡ B` and: `P ∧ Q` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` sq_type: `SQType(T)` guard: `{T}` eq_atom: `x =a y` ifthenelse: `if b then t else f fi ` tree_node?: `tree_node?(v)` pi1: `fst(t)` assert: `↑b` bfalse: `ff` false: `False` exists: `∃x:A. B[x]` prop: `ℙ` or: `P ∨ Q` bnot: `¬bb` tree_node-right: `tree_node-right(v)` pi2: `snd(t)`
Lemmas referenced :  tree-ext eq_atom_wf bool_wf eqtt_to_assert assert_of_eq_atom subtype_base_sq atom_subtype_base eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_atom assert_wf tree_node?_wf tree_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality promote_hyp productElimination hypothesis_subsumption hypothesis applyEquality sqequalRule tokenEquality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry independent_isectElimination instantiate cumulativity atomEquality dependent_functionElimination independent_functionElimination because_Cache voidElimination dependent_pairFormation universeEquality

Latex:
\mforall{}[E:Type].  \mforall{}[v:tree(E)].    tree\_node-right(v)  \mmember{}  tree(E)  supposing  \muparrow{}tree\_node?(v)

Date html generated: 2017_10_01-AM-08_30_32
Last ObjectModification: 2017_07_26-PM-04_24_37

Theory : tree_1

Home Index