Make "unused" proof arguments irrelevant
Created by: joaopizani
From @joaopizani on June 20, 2014 15:56
Such as:
-
The proof that n and m are different
Atom
indices in the Synth sum instance -
Proofs for the bijective enumeration of
Atom
-
Proofs that
Synth
is an isomorphism
Copied from original issue: joaopizani/piware#19