Thm* da:k:Knd fp-> Type, k:{k:Knd| k dom(da) & isrcv(k) }.
Thm* da-outlink-f(da;k) IdLnk Id Type | [da-outlink-f_wf] |
Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top.
Thm* f g(x)?z ~ if x dom(f) f(x)?z else g(x)?z fi | [fpf-join-cap-sq] |
Thm* B,C:(A Type), eq:EqDecider(A), f:a:A fp-> B(a), g:a:A fp-> C(a), x:A.
Thm* x dom(f)  f g(x) = f(x) B(x) | [fpf-join-ap-left] |
Thm* B:(A Type), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A.
Thm* x dom(f g)  f g(x) = if x dom(f) f(x) else g(x) fi B(x) | [fpf-join-ap] |
Thm* A:Type, B:(A Type), f:a:A fp-> B(a), eq:EqDecider(A), x:A,
Thm* P:(a:{a:A| a dom(f) } B(a) Prop). z != f(x) ==> P(x,z) Prop | [fpf-val_wf] |