(14steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc

At: discrete equality unique

T:Type, f1,f2:{T=}. f1 = f2 TT
By: UnivCD
Generated subgoal:

11. T: Type
2. f1: {T=}
3. f2: {T=}
f1 = f2 TT

About:
boolfunctionuniverseequalall

(14steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc