DEFINITION ty3_nf2_inv_abst_premise()
TYPE =
C
→
T
→
T
→
Prop
BODY =
Show proof