KimayaBedarkar
Results
2
comments of
KimayaBedarkar
> This change is indeed not consistent with many lemmas. The hypotheses of the form `_ nat) : (forall t, t1 t1 \sum_(t1
I am also a bit confused about why the operator type is an explicit parameter. Why is this needed to be explicit?