Next Types Are Theorems; Programs Are Proofs 23

Proofs with ∨


Next Next