| | Who Cites vc concl? |
|
| vc_concl | Def vc_concl(v) == Case(v) Case vc_imp(x) = > x.concl Case vc_qimp(x) = > x.concl Default = > False |
| | | Thm*  v:vc{i:l}(). vc_concl(v)  Fmla |
|
| case_default | Def Default = > body(value,value) == body |
|
| qimp_concl | Def t.concl == 2of(2of(t)) |
| | | Thm* t:qimp{i:l}(). t.concl Fmla |
|
| case_vc_qimp | Def Case vc_qimp(x) = > body(x) cont(x1,z) == ( x1.inr(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x1]) |
|
| imp_concl | Def t.concl == 2of(t) |
| | | Thm* t:imp{i:l}(). t.concl Fmla |
|
| case_vc_imp | Def Case vc_imp(x) = > body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z)) |
|
| case | Def Case(value) body == body(value,value) |
|
| pi2 | Def 2of(t) == t.2 |
| | | Thm* A:Type, B:(A  Type), p:(a:A B(a)). 2of(p) B(1of(p)) |
|
| hd | Def hd(l) == Case of l; nil  "?" ; h.t h |
| | | Thm* A:Type, l:A List. ||l|| 1   hd(l) A |
| | | Thm* A:Type, l:A List . hd(l) A |
|
| tl | Def tl(l) == Case of l; nil nil ; h.t t |
| | | Thm* A:Type, l:A List. tl(l) A List |
|
| case_inr | Def inr(x) = > body(x) cont(value,contvalue) == InjCase(value; _. cont(contvalue,contvalue); x. body(x)) |
