A,B:Type, a:EqDecider(A), b:EqDecider(B).
Thm* sum-deq(A;B;a;b)
(p,q:A+B. p = q 
sumdeq(a;b)(p,q))A,B:Type{i}, a:EqDecider(A), b:EqDecider(B).
Thm* sum-deq-aux{\\\\v:l,i:l}(A;B;a;b)
(p,q:A+B. p = q sumdeq(a;b)(p,q))| Theorem | Name |
| A,B:Type, a:EqDecider(A), b:EqDecider(B).
Thm* sum-deq(A;B;a;b) (p,q:A+B. p = q sumdeq(a;b)(p,q)) | [sum-deq_wf] |
| cites the following: | |
| A,B:Type{i}, a:EqDecider(A), b:EqDecider(B).
Thm* sum-deq-aux{\\\\v:l,i:l}(A;B;a;b) (p,q:A+B. p = q sumdeq(a;b)(p,q)) | [sum-deq-aux_wf] |