T,T':Type, x:Id, c:T, a:Id, P:(T
T'Prop).
Thm* ma-single-pre-init1(x;T;c;a;T';x,v.P(x,v))
MsgAd:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true
| Theorem | Name |
| T,T':Type, x:Id, c:T, a:Id, P:(TT'Prop).
Thm* ma-single-pre-init1(x;T;c;a;T';x,v.P(x,v)) MsgA | [ma-single-pre-init1_wf] |
| cites the following: | |
| d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true | [eqof_eq_btrue] |