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