DISP	signature_df	Signature{ < i:level > }()== Signature{ < i > }() EdAlias sign :: Sign== Sign
ABS	signature	Sign == nam: cor:(nam ) c:(n:nam cor n) idx:(nam ) fld:(n:nam idx n nam) eq_nam:(nam nam ) eq_cor:(n1:nam cor n1 n2:nam cor n2 ) (n1:nam idx n1 n2:nam idx n2 )
THM	signature_wf	Sign '
DISP	sign_nam_df	Nam( < s:sign:E > )== Nam Nam== Nam
ABS	sign_nam	Nam == s.1
THM	sign_nam_wf	s:Sign. Nam
DISP	sign_cor_df	Cor( < s:sign:E > )== Cor Cor== Cor
ABS	sign_cor	Cor == s.2.1
THM	sign_cor_wf	s:Sign. Cor Nam
DISP	sign_c_df	cor( < s:sign:E > )== cor cor== cor
ABS	sign_c	cor == s.2.2.1
THM	sign_c_wf	s:Sign. cor n:Nam Cor n
DISP	sign_idx_df	Idx( < s:sign:E > )== Idx Idx== Idx
ABS	sign_idx	Idx == s.2.2.2.1
THM	sign_idx_wf	s:Sign. Idx Nam
DISP	sign_fld_df	Fld( < s:sign:E > )== Fld Fld== Fld
ABS	sign_fld	Fld == s.2.2.2.2.1
THM	sign_fld_wf	s:Sign. Fld n:Nam Idx n Nam
DISP	sign_eq_nam_df	EqNam( < s:sign:E > )== EqNam EqNam== EqNam
ABS	sign_eq_nam	EqNam == s.2.2.2.2.2.1
THM	sign_eq_nam_wf	s:Sign. EqNam Nam Nam
DISP	sign_eq_cor_df	EqCor( < s:sign:E > )== EqCor EqCor== EqCor
ABS	sign_eq_cor	EqCor == s.2.2.2.2.2.2.1
THM	sign_eq_cor_wf	s:Sign. EqCor n1:Nam Cor n1 n2:Nam Cor n2
DISP	sign_eq_idx_df	EqIdx( < s:sign:E > )== EqIdx EqIdx== EqIdx
ABS	sign_eq_idx	EqIdx == s.2.2.2.2.2.2.2
THM	sign_eq_idx_wf	s:Sign. EqIdx n1:Nam Idx n1 n2:Nam Idx n2
ML	create_signature	Class Declaration for: s Sign Long Name: signature Short Name: sign Parameters: Fields: (Nam) nam : (Cor) cor : nam (cor) c : n:nam cor n (Idx) idx : nam (Fld) fld : n:nam idx n nam (EqNam) eq_nam : nam nam (EqCor) eq_cor : n1:nam cor n1 n2:nam cor n2 (EqIdx) eq_idx : n1:nam idx n1 n2:nam idx n2 Universe: '
DISP	eq_nam_df	( < n1:nam:* > = < n2:nam:* > wrt < s:sign:* > )== ( < n1 > = < n2 > ) ( < n1:nam:* > = < n2:nam:* > )== ( < n1 > = < n2 > )
ABS	eq_nam	(n1 = n2) == EqNam n1 n2
THM	eq_nam_wf	s:Sign. n,k:Nam. (n = k)
DISP	eq_cor_df	( < c1:term:* > :Cor( < n1:nam:* > ) = < c2:term:* > :Cor( < n2:nam:* > ) wrt < s:sign:* > ) == ( < c1 > = < c2 > ) ( < c1:term:* > = < c2:term:* > )== ( < c1 > = < c2 > )
ABS	eq_cor	(c1 = c2) == EqCor n1 c1 n2 c2
THM	eq_cor_wf	s:Sign. n1,n2:Nam. c1:Cor n1. c2:Cor n2. (c1 = c2)
DISP	eq_idx_df	( < i1:idx:* > :Idx( < n1:nam:* > ) = < i2:idx:* > :Idx( < n2:nam:* > ) wrt < s:sign:* > ) == ( < i1 > = < i2 > ) ( < i1:idx:* > = < i2:idx:* > )== ( < i1 > = < i2 > )
ABS	eq_idx	(i1 = i2) == EqIdx n1 i1 n2 i2
THM	eq_idx_wf	s:Sign. n1,n2:Nam. i1:Idx n1. i2:Idx n2. (i1 = i2)
DISP	reg_sign_df	Reg( < s:sign:* > )== Reg( < s > )
ABS	reg_sign	Reg(s) == (n,k:Nam. (n = k) n = k) (n,k:Nam. c:Cor n. d:Cor k. (c = d) (n = k) c (c = d)) (n,k:Nam. i:Idx n. j:Idx k. (i = j) (n = k) c (i = j))
THM	reg_sign_wf	s:Sign. Reg(s)

the other theories