a:Id, T,A:Type, x:Id, P:(A
TProp).
Thm* ma-single-pre1(x;A;a;T;x,v.P(x,v))
MsgAd:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true
| Theorem | Name |
| a:Id, T,A:Type, x:Id, P:(ATProp).
Thm* ma-single-pre1(x;A;a;T;x,v.P(x,v)) MsgA | [ma-single-pre1_wf] |
| cites the following: | |
| d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true | [eqof_eq_btrue] |