Nuprl Lemma : oobleft-lval_wf
∀[A,B:Type]. ∀[x:one_or_both(A;B)]. oobleft-lval(x) ∈ A supposing ↑oobleft?(x)
Proof
Error : references
Latex:
\mforall{}[A,B:Type]. \mforall{}[x:one\_or\_both(A;B)]. oobleft-lval(x) \mmember{} A supposing \muparrow{}oobleft?(x)
Date html generated:
2020_05_20-AM-08_41_14
Last ObjectModification:
2020_02_01-AM-08_16_31
Theory : general
Home
Index