Nuprl Lemma : l_tree_node-left_subtree_wf

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


Proof




Definitions occuring in Statement :  l_tree_node-left_subtree: l_tree_node-left_subtree(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-left\_subtree(v)  \mmember{}  l\_tree(L;T)  supposing  \muparrow{}l\_tree\_node?(v)



Date html generated: 2015_07_17-AM-07_41_36
Last ObjectModification: 2015_01_27-AM-09_31_04

Home Index