Nuprl Lemma : l_tree_node-val_wf

[L,T:Type]. ∀[v:l_tree(L;T)].  l_tree_node-val(v) ∈ supposing ↑l_tree_node?(v)


Proof




Definitions occuring in Statement :  l_tree_node-val: l_tree_node-val(v) l_tree_node?: l_tree_node?(v) l_tree: l_tree(L;T) assert: b uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T universe: Type
Lemmas :  l_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 l_tree_node?_wf l_tree_wf
\mforall{}[L,T:Type].  \mforall{}[v:l\_tree(L;T)].    l\_tree\_node-val(v)  \mmember{}  T  supposing  \muparrow{}l\_tree\_node?(v)



Date html generated: 2015_07_17-AM-07_41_34
Last ObjectModification: 2015_01_27-AM-09_31_06

Home Index